proposition: Lemma mults_order_l : forall l m1 m2, ~ zeroP (A:=A) A0 eqA (n:=n) m1 -> canonical A0 eqA ltM (pX m2 l) -> canonical A0 eqA ltM (pX (multTerm (A:=A) multA (n:=n) m1 m2) (mults m1 l)).
proof: Proof. Proof using plusA os minusA invA eqA_dec divA cs A1. intros l; elim l; simpl in |- *; auto. intros m1 m2 H' H'0. apply canonicalp1; auto. red in |- *; intros H'1; apply H'. elim multTerm_zeroP_div with (1 := cs) (a := m1) (b := m2); auto; intros H'5. absurd (zeroP (A:=A) A0 eqA (n:=n) m2); auto. apply canonical_nzeroP with (ltM := ltM) (p := pO A n); auto. intros a l0 H' m1 m2 H'0 H'1. apply canonical_cons; auto. apply multTerm_ltT_l; auto. apply (canonical_pX_order A A0 eqA) with (l := l0); auto. red in |- *; intros H'2; apply H'0. elim multTerm_zeroP_div with (1 := cs) (a := m1) (b := m2); auto; intros H'5. absurd (zeroP (A:=A) A0 eqA (n:=n) m2); auto. apply canonical_nzeroP with (ltM := ltM) (p := pX a l0); auto. apply H'; auto. apply canonical_imp_canonical with (a := m2); auto. Qed.