proposition: Lemma add_sub_add_l : forall n m p : nat, (n - m) = (p + n - (p + m)).
proof: Proof. intros n m p; induction p as [| p IH]. - by rewrite 2!Nat.add_0_l. - by rewrite 2!Nat.add_succ_l Nat.sub_succ IH. Qed.
imports: Coq(Reals Psatz ssreflect)