proposition: Proposition add_n_sub_n_eq (m n : nat) : m + n - n = m.
proof: Proof. destruct m. - simple_induction' n. + reflexivity. + assumption. - simple_induction' n. + simpl. destruct (add_n_O m); reflexivity. + simpl. destruct (add_n_Sm m n). assumption. Defined.
imports: Basics Spaces.Nat.Core