proposition: Theorem zerop_is_eqTerm : forall a b : Term A n, eqT a b -> zeroP (A:=A) A0 eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) -> eqTerm (A:=A) eqA (n:=n) a b.
proof: Proof. Proof using plusA multA invA divA cs A1. intros a b H' H'0. cut (eqT a (invTerm (A:=A) invA (n:=n) b)); [ intros eq1 | idtac ]. cut (eqT a (plusTerm (A:=A) plusA (n:=n) b (invTerm (A:=A) invA (n:=n) b))); [ intros eq2 | idtac ]. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a (plusTerm (A:=A) plusA (n:=n) b (invTerm (A:=A) invA (n:=n) b))); auto. apply zeroP_plusTermr with (1 := cs); auto. apply plusTerm_invTerm_zeroP with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a (plusTerm (A:=A) plusA (n:=n) (invTerm (A:=A) invA (n:=n) b) b)); auto. apply plusTerm_comp_r with (1 := cs); auto. apply (eqT_trans A n) with (plusTerm plusA b (invTerm invA b)); auto. apply (eqTerm_imp_eqT A eqA); auto. apply plusTerm_com with (1 := cs); auto. apply plusTerm_com with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a (invTerm (A:=A) invA (n:=n) b)) b); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply plusTerm_assoc with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply zeroP_plusTerml with (1 := cs); auto. apply (eqT_trans A n) with (invTerm invA b); auto. apply plusTerm_eqT2; auto. apply (eqT_sym A n); apply invTerm_eqT; auto. apply zeroP_comp_eqTerm with (1 := cs) (2 := H'0). apply eqTerm_minusTerm_plusTerm_invTerm with (1 := cs); auto. apply (eqT_trans A n) with (1 := eq1); auto. apply (eqT_sym A n); apply plusTerm_eqT2; auto. apply (eqT_trans A n) with (1 := H'); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)