proposition: Theorem minus_O_le : forall n m : nat, n - m = 0 -> n <= m.
proof: Proof. intros n; elim n; clear n. auto with arith. intros n Hrec m; case m; clear m. simpl in |- *; intros Heq; discriminate Heq. simpl in |- *; intros; apply le_n_S; apply Hrec; auto. Qed.