proposition: Theorem eqTerm_spminusf_com : forall (a b c : Term A n) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c) (p q : list (Term A n)), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> eqTerm (A:=A) eqA (n:=n) a b -> divP A A0 eqA multA divA n a c -> eqP A eqA n (spminusf a c nZc p q) (spminusf b c nZc p q).
proof: Proof. Proof using plusA os cs. intros a b c nZc p q H' H'0 H'1 H'2. cut (divP A A0 eqA multA divA n b c); [ intros H'3 | auto ]. unfold spminusf in |- *; auto. apply divP_eqTerm_comp with (1 := cs) (a := a); auto. Qed.