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