proposition: Lemma ineq_sub (n m : nat) : n <= m -> m - (m - n) = n.
proof: Proof. revert m; simple_induction n n IHn. - intros. destruct (symmetric_paths _ _ (sub_n_0 m)), (symmetric_paths _ _ (sub_n_n m)); reflexivity. - intros m ineq. change (m - n.+1) with (m - (1 + n)). (destruct (nat_add_comm n 1)). destruct (symmetric_paths _ _ (subsubadd m n 1)). destruct (S_predn (m - n) 0 (lt_sub_gt_0 _ _ ineq)); simpl; destruct (symmetric_paths _ _ (sub_n_0 (pred (m - n)))). assert (0 < m - n) as dp by exact (lt_sub_gt_0 _ _ ineq). assert (pred (m - n) < m) as sh by ( unfold "<"; destruct (symmetric_paths _ _ (S_predn _ 0 _)); exact sub_less). destruct (symmetric_paths _ _ (ineq_sub' _ _ _)). destruct (symmetric_paths _ _ (S_predn _ 0 _)). apply (ap S), IHn, leq_S', ineq. Defined.
imports: Basics Spaces.Nat.Core