proposition: Lemma minus_le_lem2 : forall a b : nat, a - b <= a.
proof: Proof. simple induction b. elim minus_n_O. auto with arith. intros. apply le_trans with (a - n). apply minus_le_lem2c. exact H. Qed.
imports: Plus Mult Minus Lt Le Gt