proposition: Lemma minus_le_lem2c : forall a b : nat, a - S b <= a - b.
proof: Proof. intros. pattern a, b in |- *. apply nat_double_ind. auto with arith. intro. elim minus_n_O. rewrite minus_n_SO. simpl in |- *. auto with arith. intros. simpl in |- *. exact H. Qed.
imports: Plus Mult Minus Lt Le Gt