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