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