proposition: Lemma lcm_equiv2 : forall a b, (a / gcd a b) * b == (a*b)/gcd a b.
proof: Proof. intros a b. destruct (eq_decidable (gcd a b) 0) as [->|?]. - now nzsimpl. - now apply lcm_equiv2. Qed.
imports: NAxioms NSub NDiv0 NGcd NLcm