proposition: Lemma minus_le_O : forall a b : nat, a <= b -> a - b = 0.
proof: Proof. intros. pattern a, b in |- *. apply le_elim_rel. auto with arith. intros. simpl in |- *. exact H1. exact H. Qed.
imports: Plus Mult Minus Lt Le Gt