(* we now close all positivity conditions *)
apply lt_O_times_S_S.
apply lt_O_times_S_S.
-simplify.
+simplify.unfold lt.
apply le_SO_minus. exact H.
qed.
(pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
intros.
simplify.
-change in match p + n * (S p) with (pred ((S n) * (S p))).
-change in match q + n * (S q) with (pred ((S n) * (S q))).
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.