- |@sym_eq (applyS plus_to_minus) <(distributive_times_plus …)
- (* STRANO *)
- @(eq_f …b) (applyS plus_minus_m_m) /2/
+ |@sym_eq (applyS plus_to_minus) <distributive_times_plus
+ @eq_f (applyS plus_minus_m_m) /2/
+qed.
+
+theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
+#n #m #p
+cases (decidable_le (m+p) n) #Hlt
+ [@plus_to_minus @plus_to_minus <associative_plus
+ @minus_to_plus //
+ |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
+ #H >eq_minus_O /2/ >eq_minus_O //
+ ]
+qed.
+
+(*
+theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus <plus_minus_m_m //
+qed. *)
+
+theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
+ p+(n-m) = n-(m-p).
+#n #m #p #lepm #lemn
+@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
+<commutative_plus <plus_minus_m_m //