proposition: Proposition natminuspluseq (n m : nat) : n <= m -> (m - n) + n = m.
proof: Proof. revert m; simple_induction n n IHn. - intros. destruct m; [reflexivity |]. simpl. apply (ap S), symmetric_paths, add_n_O. - intros m l. destruct m. + contradiction (not_leq_Sn_0 n). + simpl. apply leq_S_n, IHn in l. destruct (nat_add_n_Sm (m - n) n). destruct (symmetric_paths _ _ l). reflexivity. Defined.
imports: Basics Spaces.Nat.Core