proposition: Lemma ring_sub_ext : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
proof: Proof. intros. setoid_replace (x1 - y1) with (x1 + -y1). - setoid_replace (x2 - y2) with (x2 + -y2). + rewrite H;rewrite H0;reflexivity. + rewrite ring_sub_def. reflexivity. - rewrite ring_sub_def. reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax