proposition: Lemma lcm_least : forall a b c, (a | c) -> (b | c) -> (lcm a b | c).
proof: Proof. intros a b c Ha Hb. unfold lcm. destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. - apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ in *. now nzsimpl. - assert (Ga := gcd_divide_l a b). assert (Gb := gcd_divide_r a b). set (g:=gcd a b) in *. assert (Ha' := divide_div g a c NEQ Ga Ha). assert (Hb' := divide_div g b c NEQ Gb Hb). destruct Ha' as (a',Ha'). rewrite Ha', mul_comm in Hb'. apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm]. destruct Hb' as (b',Hb'). exists b'. rewrite mul_shuffle3, <- Hb'. rewrite (proj2 (div_exact c g NEQ)). + rewrite Ha', mul_shuffle3, (mul_comm a a'). f_equiv. symmetry. apply div_exact; trivial. apply mod_divide; trivial. + apply mod_divide; trivial. transitivity a; trivial. Qed.
imports: NAxioms NSub NDiv NGcd