proposition: Theorem plus_minus_le : forall a b : nat, a - b + b = a -> b <= a.
proof: Proof. intros a; elim a; simpl in |- *; auto. intros b H'; rewrite H'; auto. intros n H' b; case b; simpl in |- *; auto with arith. intros n0; rewrite (Nat.add_comm (n - n0) (S n0)); simpl in |- *; auto. rewrite (Nat.add_comm n0 (n - n0)); auto with arith. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)