proposition: Lemma canonical_mults_inv : forall (p : list (Term A n)) (a : Term A n), ~ zeroP (A:=A) A0 eqA (n:=n) a -> canonical A0 eqA ltM (mults a p) -> canonical A0 eqA ltM p.
proof: Proof. Proof using plusA os minusA ltM_dec invA divA cs A1. intros p; elim p; simpl in |- *; auto. intros a l; case l; simpl in |- *; auto. intros H' a0 H'0 H'1. change (canonical A0 eqA ltM (pX a (pO A n))) in |- *; apply canonicalp1; auto. red in |- *; intros H'2; absurd (zeroP (A:=A) A0 eqA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a)); auto. apply canonical_nzeroP with (ltM := ltM) (p := pO A n); auto. intros a0 l0 H' a1 H'0 H'1. change (canonical A0 eqA ltM (pX a (pX a0 l0))) in |- *. apply canonical_cons; auto. case (ltT_dec A n ltM ltM_dec a0 a); [ intros temp; case temp; clear temp | idtac ]; intros H; auto. absurd (ltT ltM (multTerm (A:=A) multA (n:=n) a1 a) (multTerm (A:=A) multA (n:=n) a1 a0)); auto. apply ltT_not_ltT; auto. apply (canonical_pX_order A A0 eqA) with (l := mults a1 l0); auto. apply multTerm_ltT_l with (1 := os); auto. absurd (ltT ltM (multTerm (A:=A) multA (n:=n) a1 a0) (multTerm (A:=A) multA (n:=n) a1 a)); auto. apply (canonical_pX_order A A0 eqA) with (l := mults a1 l0); auto. red in |- *; intros H'2; absurd (zeroP (A:=A) A0 eqA (n:=n) (multTerm (A:=A) multA (n:=n) a1 a)); auto. apply canonical_nzeroP with (ltM := ltM) (p := mults a1 l0); auto. apply canonical_skip_fst with (b := multTerm (A:=A) multA (n:=n) a1 a0); auto. apply H' with (a := a1); auto. apply canonical_imp_canonical with (a := multTerm (A:=A) multA (n:=n) a1 a); auto. Qed.