proposition: Proposition nataddsub_assoc (n : nat) {m k : nat} : (k <= m) -> n + (m - k) = n + m - k.
proof: Proof. revert m k. simple_induction n n IHn. - reflexivity. - intros m k l. change (n.+1 + (m - k)) with (n + (m - k)).+1; change (n.+1 + m) with (n +m).+1. destruct k, m; [ reflexivity | reflexivity | contradiction (not_lt_n_0 k _) | ]. simpl "-". apply leq_S_n in l. destruct (symmetric_paths _ _ (nat_add_n_Sm n (m - k))). destruct (nataddsub_assoc_lemma l). apply (IHn m.+1 k). apply leq_S. assumption. Defined.
imports: Basics Spaces.Nat.Core