proposition: Lemma minusP_is_plusP_mults : forall p q r : list (Term A n), minusP p q r -> eqP A eqA n r (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) q)).
proof: Proof. Proof using os divA cs. intros p q r H'; elim H'; auto. intros; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. simpl in |- *; intros; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX a1 (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l1 (pX (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) l2)))); auto. simpl in |- *; apply pluspf_inv1 with (1 := cs); auto. change (ltT ltM (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2) a1) in |- *. apply eqT_compat_ltTl with (b := a2); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2 H'3. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l1 (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) l2)); auto. simpl in |- *; apply pluspf_inv3a with (1 := cs); auto. change (eqT a1 (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2)) in |- *. apply (eqT_trans A n) with (y := a2); auto. change (zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2))) in |- *; auto. apply zeroP_comp_eqTerm with (1 := cs) (a := minusTerm (A:=A) minusA (n:=n) a1 a2); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (invTerm (A:=A) invA (n:=n) a2)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply plusTerm_comp_r with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) a2)); auto. apply eqTerm_invTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2 H'3. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX (plusTerm (A:=A) plusA (n:=n) a1 (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2)) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l1 (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) l2))); auto. apply eqpP1; auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (invTerm (A:=A) invA (n:=n) a2)); auto. apply plusTerm_comp_r with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) a2)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. simpl in |- *; apply pluspf_inv3b with (1 := cs); auto. change (eqT a1 (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2)) in |- *. apply (eqT_trans A n) with (y := a2); auto. change (~ zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2))) in |- *; auto. apply nzeroP_comp_eqTerm with (1 := cs) (a := minusTerm (A:=A) minusA (n:=n) a1 a2); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (invTerm (A:=A) invA (n:=n) a2)); auto. apply plusTerm_comp_r with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) a2)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a1 a2 l1 l2 l3 H'0 H'1 H'2. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pX a1 l1) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) l2))); auto. apply eqpP1; auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) a2)); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. simpl in |- *; apply pluspf_inv2 with (1 := cs); auto. change (ltT ltM a1 (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a2)) in |- *; auto. apply eqT_compat_ltTr with (b := a2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)