proposition: Theorem le_diff_le : forall n m:nat, le_diff n m -> n <= m.
proof: Proof. intros n m [x]. generalize H. clear H. generalize m. clear m. induction x as [ | y Hy]. - intros m e ; rewrite <- e; constructor. - intros m e. subst m; simpl; auto. Qed.
imports: Setoid