(n m : nat) : n <= m -> m - (m - n) = n. Proof. revert m; simple_induction n n IHn. - intros. destruct (symmetric_paths _ _ (nat_sub_zero_r m)), (symmetric_paths _ _ (nat_sub_cancel m)); reflexivity. - intros m ineq. change (m - n.+1) with (m - (1 + n)). (destruct (nat_add_comm n 1)). destruct (symmetric_paths _ _ (nat_sub_r_add m n 1)). destruct (nat_succ_pred (m - n) (equiv_lt_lt_sub _ _ ineq)); simpl; destruct (symmetric_paths _ _ (nat_sub_zero_r (nat_pred (m - n)))). assert (0 < m - n) as dp by exact (equiv_lt_lt_sub _ _ ineq). assert (nat_pred (m - n) < m) as sh by ( unfold "<"; destruct (symmetric_paths _ _ (nat_succ_pred _ _)); exact sub_less). destruct (symmetric_paths _ _ (' _ _ _)). destruct (symmetric_paths _ _ (nat_succ_pred _ _)). apply (ap S), IHn, leq_succ_l, ineq. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.