proposition: Proposition nataddsub_assoc_lemma {k m : nat} : (k <= m) -> m.+1 - k = (m - k).+1.
proof: Proof. revert m; simple_induction k k IHk. - intros m l; simpl. destruct m; reflexivity. - destruct m. + simpl; intro g; contradiction (not_leq_Sn_0 _ g). + intro l; apply leq_S_n in l. change (m.+2 - k.+1) with (m.+1 - k). change (m.+1 - k.+1) with (m - k). exact (IHk _ l). Defined.
imports: Basics Spaces.Nat.Core