Some lemmas about divisibility

File SRC/chap7.v contains some admitted lemmas about divisibility. Please replace the Admitted commands with complete proofs.

Solution

Look at this file