proposition: Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a.
proof: Proof. intros a b Hb. rewrite (gcd_comm _ b). rewrite <- (gcd_add_mult_diag_r b (a mod b) (a/b)). now rewrite add_comm, mul_comm, <- div_mod. Qed.
imports: NAxioms NSub NDiv NGcd