proposition: Theorem multTerm_or_z_d2 : forall (a b : Term A n) (nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b) (p : list (Term A n)), canonical A0 eqA ltM (pX a p) -> forall c : Term A n, In c (mults (A:=A) multA (n:=n) b p) -> ltT ltM c (multTerm (A:=A) multA (n:=n) b a) /\ eqT c (multTerm (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) c (b:=b) nZb) b).
proof: Proof. Proof using plusA os minusA invA cs A1. intros a b H' p; elim p; simpl in |- *; auto. intros H'0 c H'1; elim H'1. intros a0 l H'0 H'1 c H'2; elim H'2; [ intros H'3; rewrite <- H'3; clear H'2 | intros H'3; clear H'2 ]; auto. 2: apply H'0; auto. 2: apply canonical_skip_fst with (b := a0); auto. split; auto. apply multTerm_ltT_l; auto. apply (canonical_pX_order A A0 eqA) with (l := l); auto. apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) a0 b); auto. apply (eqTerm_imp_eqT A eqA); auto. apply multTerm_eqT; auto. apply (eqTerm_imp_eqT A eqA); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) b (b:=b) H') a0); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.