proposition: Lemma b_d : forall a b : nat, bezout a b -> bezout a (a + b)%nat.
proof: Proof. intros a b H; case H. intros u v H0 HA e. split with (u-v) v. - auto. - auto with zarith. - rewrite inj_plus; ring_simplify; now rewrite (Zmult_comm v (Z_of_nat b)). Qed.
imports: ZArith