proposition: Theorem eqp_spminusf_com : forall (a b c : Term A n) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c) (p q r : list (Term A n)), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> eqP A eqA n p 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 r) (spminusf b c nZc q r).
proof: Proof. Proof using plusA os cs. intros a b c nZc p q r H' H'0 H'1 H'2 H'3 H'4. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := spminusf b c nZc p r); auto. apply eqTerm_spminusf_com; auto. apply eqptail_spminusf_com; auto. apply divP_eqTerm_comp with (1 := cs) (a := a); auto. Qed.