proposition: Theorem multpf_comp : forall p r : list (Term A n), eqP A eqA n p r -> forall q s : list (Term A n), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> canonical A0 eqA ltM s -> eqP A eqA n q s -> eqP A eqA n (multpf p q) (multpf r s).
proof: Proof. Proof using os minusA invA divA cs A1. intros p r H'; elim H'; simpl in |- *; auto. intros ma mb p0 q H'0 H'1 H'2 q0 s H'3 H'4 H'5 H'6 H'7. cut (canonical A0 eqA ltM p0); [ intros Op0 | apply canonical_imp_canonical with (a := ma); auto ]. cut (canonical A0 eqA ltM q); [ intros Op1 | apply canonical_imp_canonical with (a := mb); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) ma); [ intros Z0 | apply canonical_nzeroP with (ltM := ltM) (p := p0); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) mb); [ intros Z1 | apply canonical_nzeroP with (ltM := ltM) (p := q) ]; auto. Qed.