proposition: Theorem canonical_multpf : forall l1 l2 : list (Term A n), canonical A0 eqA ltM l1 -> canonical A0 eqA ltM l2 -> canonical A0 eqA ltM (multpf l1 l2).
proof: Proof. Proof using os minusA invA divA cs A1. intros l1; elim l1; simpl in |- *; auto. intros a l H' l2 H'0 H'1; try assumption. apply canonical_pluspf; auto. apply canonical_mults with (1 := cs); auto. apply canonical_nzeroP with (ltM := ltM) (p := l); auto. apply H'; auto. apply canonical_imp_canonical with (a := a); auto. Qed.