proposition: Lemma gcd_sub_diag_r : forall n m, gcd n (m-n) == gcd n m.
proof: Proof. intros n m. rewrite <- (mul_1_l n) at 2. rewrite <- add_opp_r, <- mul_opp_l. apply gcd_add_mult_diag_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd