proposition: Theorem mults_invTerm : forall (p : list (Term A n)) (a : Term A n), eqTerm (A:=A) eqA (n:=n) a (T1 A1 n) -> eqP A eqA n (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p (mults (invTerm (A:=A) invA (n:=n) a) p)) (pO A n).
proof: Proof. Proof using os minusA divA cs. intros p; elim p; simpl in |- *; auto. intros a l H' a0 H'0. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l (mults (invTerm (A:=A) invA (n:=n) a0) l)); auto. change (eqP A eqA n (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pX a l) (pX (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) a0) a) (mults (invTerm (A:=A) invA (n:=n) a0) l))) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l (mults (invTerm (A:=A) invA (n:=n) a0) l))) in |- *. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply pluspf_inv3a with (1 := cs); auto. apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) a0 a); auto. apply (T1_eqT _ A1 eqA); auto. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a (invTerm (A:=A) invA (n:=n) a)); auto. apply plusTerm_invTerm_zeroP with (1 := cs); auto. apply plusTerm_comp_r with (1 := cs); auto. change (eqT a (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) a0) a)) in |- *. apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) a); auto. apply (T1_eqT _ A1 eqA); auto. apply multTerm_eqT; auto. apply (eqT_trans A n) with (y := a0); auto. apply (eqT_sym A n); auto. apply (eqTerm_imp_eqT A eqA); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) a (T1 A1 n))); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) a a0)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply eqTerm_invTerm_comp with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply mult_invTerm_com with (1 := cs); auto. Qed.