proposition: Theorem le_minus_O : forall n m : nat, n <= m -> n - m = 0.
proof: Proof. intros n; elim n; clear n. simpl in |- *; auto. intros n Hrec m; case m; clear m. intros Hle; inversion Hle. intros m' Hle; simpl in |- *; apply Hrec; auto with arith. Qed.