proposition: Lemma le_minus_minus : forall a b c : nat, c <= b -> a - b <= a - c.
proof: Proof. simple induction a. simpl in |- *. auto with arith. intros. generalize H0. elim c. elim minus_n_O. intro. apply minus_le_lem2. elim b. intros. absurd (S n0 <= 0). auto with arith. exact H2. intros. simpl in |- *. apply H. apply le_S_n. exact H3. Qed.
imports: Plus Mult Minus Lt Le Gt