proposition: Lemma gcd_div_swap : 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 [EQ|NEQ]. - apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ, EQ'. now nzsimpl. - now rewrite lcm_equiv1, <-lcm_equiv2. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor