proposition: Lemma eq_minus : forall a b c : nat, c < a -> a - c = b - c -> a = b.
proof: Proof. intros a b c H' H'0. rewrite <- (Nat.sub_add c a); auto with arith. rewrite <- (Nat.sub_add c b); auto with arith. apply Nat.lt_le_incl. apply (Nat.lt_add_lt_sub_r 0). rewrite <- H'0; auto. apply lt_minus_O_lt; auto. Qed.
imports: Coq(Arith ArithRing)