proposition: Theorem pluspf3_assoc : forall l, canonical A0 eqA ltM (fst l) -> canonical A0 eqA ltM (fst (snd l)) -> canonical A0 eqA ltM (snd (snd l)) -> eqP A eqA n (pluspf (pluspf (fst l) (fst (snd l))) (snd (snd l))) (pluspf (fst l) (pluspf (fst (snd l)) (snd (snd l)))).
proof: Proof. Proof using os multA minusA invA divA cs A1. intros l; pattern l in |- *. apply (well_founded_ind (wf_lessP3 A n)). intros x; case x; intros p z; case z; intros q r; simpl in |- *; clear x z; auto. case p. rewrite <- pO_pluspf_inv1; auto. case q. intros a l0; rewrite <- pO_pluspf_inv1; rewrite <- pO_pluspf_inv2; auto. case r; simpl in |- *; auto. intros a l0 a0 l1; rewrite <- pO_pluspf_inv2; rewrite <- pO_pluspf_inv2; auto. intros a l0 a0 l1 a1 l2 H' H'0 H'1 H'2. cut (canonical A0 eqA ltM (pX a l0)); [ clear H'2; intros H'2 | auto ]. cut (canonical A0 eqA ltM (pX a0 l1)); [ clear H'1; intros H'1 | auto ]. cut (canonical A0 eqA ltM (pX a1 l2)); [ clear H'0; intros H'0 | auto ]. cut (canonical A0 eqA ltM l0); [ intros C0 | apply canonical_imp_canonical with (a := a) ]; auto. cut (canonical A0 eqA ltM l1); [ intros C1 | apply canonical_imp_canonical with (a := a0) ]; auto. cut (canonical A0 eqA ltM l2); [ intros C2 | apply canonical_imp_canonical with (a := a1) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros nZ0 | apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := l0) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); [ intros nZ1 | apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := l1) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a1); [ intros nZ2 | apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := l2) ]; auto. change (eqP A eqA n (pluspf (pluspf (pX a1 l2) (pX a0 l1)) (pX a l0)) (pluspf (pX a1 l2) (pluspf (pX a0 l1) (pX a l0)))) in |- *. case (ltT_dec A n ltM ltM_dec a1 a0); [ intros H0; case H0; clear H0 | idtac ]; intros H0. case (ltT_dec A n ltM ltM_dec a0 a); [ intros H1; case H1; clear H1 | idtac ]; intros H1. cut (ltT ltM a1 a); [ intros Ord0 | apply (ltT_trans A _ _ os) with (y := a0) ]; auto. rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); auto. rewrite <- (pluspf_inv2_eq a0 a (pluspf (pX a1 l2) l1) l0); auto. rewrite <- (pluspf_inv2_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. apply eqpP1; auto. rewrite (pluspf_inv2_eq a1 a0 l2 l1); auto. apply H' with (y := (pX a1 l2, (pX a0 l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. repeat rewrite (fun a b : nat => Nat.add_comm a (S b)); simpl in |- *. repeat rewrite (Nat.add_comm (size A n l1)); auto. rewrite <- (pluspf_inv1_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); auto. rewrite <- (pluspf_inv2_eq a1 a0 l2 (pluspf l1 (pX a l0))); auto. rewrite <- (pluspf_inv1_eq a0 a (pluspf (pX a1 l2) l1) l0); auto. apply eqpP1; auto. apply H' with (y := (pX a1 l2, (l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. cut (ltT ltM a1 a); [ intros Ord0 | apply eqT_compat_ltTr with (b := a0) ]; auto. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a0 a)); intros Z0. rewrite <- (pluspf_inv3a_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); auto. rewrite <- (pluspf_inv3a_eq a0 a (pluspf (pX a1 l2) l1) l0); auto. apply H' with (y := (pX a1 l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. repeat rewrite (fun a b : nat => Nat.add_comm a (S b)); simpl in |- *. repeat rewrite (Nat.add_comm (size A n l2)); auto. repeat rewrite (Nat.add_comm (size A n l1)); auto. cut (ltT ltM a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); [ intros Ord1 | apply eqT_compat_ltTr with (b := a0); auto; apply (eqT_sym A n); apply (plusTerm_eqT1 A plusA n) ]; auto. rewrite <- (pluspf_inv2_eq a1 a0 l2 l1); auto. rewrite <- (pluspf_inv3b_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv3b_eq a0 a (pluspf (pX a1 l2) l1) l0); auto. rewrite <- (pluspf_inv2_eq a1 (plusTerm (A:=A) plusA (n:=n) a0 a) l2 (pluspf l1 l0)) ; auto. apply eqpP1; auto. apply H' with (y := (pX a1 l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. repeat rewrite (fun a b : nat => Nat.add_comm a (S b)); simpl in |- *. repeat rewrite (Nat.add_comm (size A n l2)); auto. repeat rewrite (Nat.add_comm (size A n l1)); auto. rewrite <- (pluspf_inv1_eq a1 a0 l2 l1); auto. case (ltT_dec A n ltM ltM_dec a0 a); [ intros H1; case H1; clear H1 | idtac ]; intros H1. rewrite <- (pluspf_inv2_eq a0 a l1 l0); auto. case (ltT_dec A n ltM ltM_dec a1 a); [ intros H2; case H2; clear H2 | idtac ]; intros H2. rewrite <- (pluspf_inv2_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. apply eqpP1; auto. rewrite (pluspf_inv1_eq a1 a0 l2 l1); auto. apply H' with (y := (pX a1 l2, (pX a0 l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. repeat rewrite (fun a b : nat => Nat.add_comm a (S b)); simpl in |- *. repeat rewrite (Nat.add_comm (size A n l1)); auto. rewrite <- (pluspf_inv1_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. apply eqpP1; auto. rewrite (pluspf_inv2_eq a0 a l1 l0); auto. apply H' with (y := (l2, (pX a0 l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto. cut (ltT ltM a0 (plusTerm (A:=A) plusA (n:=n) a1 a)); [ intros Ord1 | apply eqT_compat_ltTr with (b := a1); auto; apply (eqT_sym A n); apply (plusTerm_eqT1 A plusA n) ]; auto. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a1 a)); intros Z0. rewrite <- (pluspf_inv3a_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. rewrite <- (pluspf_inv3a_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. apply H' with (y := (l2, (pX a0 l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. rewrite <- (pluspf_inv3b_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. rewrite <- (pluspf_inv3b_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. apply eqpP1; auto. apply H' with (y := (l2, (pX a0 l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. cut (ltT ltM a a1); [ intros Ord0 | apply (ltT_trans A n ltM os) with (y := a0) ]; auto with arith. rewrite <- (pluspf_inv1_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv1_eq a1 a0 l2 (pluspf l1 (pX a l0))); auto. rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. apply eqpP1; auto. rewrite (pluspf_inv1_eq a0 a l1 l0); auto. apply H' with (y := (l2, (pX a0 l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto. cut (ltT ltM a a1); [ intros Ord0 | apply eqT_compat_ltTl with (b := a0); auto ]; auto. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a0 a)); intros Z0. rewrite <- (pluspf_inv3a_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv1_eqa a1 l2 (pluspf l1 l0)); auto. rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. apply eqpP1; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf l2 (pluspf (pX a0 l1) (pX a l0))); auto. apply H' with (y := (l2, (pX a0 l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto. rewrite <- (pluspf_inv3a_eq a0 a l1 l0); auto. apply order_pluspf; auto. apply canonical_skip_fst with (b := a0); auto. apply canonical_skip_fst with (b := a); auto. cut (ltT ltM (plusTerm (A:=A) plusA (n:=n) a0 a) a1); [ intros Ord1 | apply eqT_compat_ltTl with (b := a0); auto; apply (eqT_sym A n); auto; apply (plusTerm_eqT1 A plusA n) ]; auto. rewrite <- (pluspf_inv3b_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv1_eq a1 a (pluspf l2 (pX a0 l1)) l0); auto. rewrite <- (pluspf_inv1_eq a1 (plusTerm (A:=A) plusA (n:=n) a0 a) l2 (pluspf l1 l0)) ; auto. apply eqpP1; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf l2 (pluspf (pX a0 l1) (pX a l0))); auto. apply H' with (y := (l2, (pX a0 l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto. rewrite <- (pluspf_inv3b_eq a0 a l1 l0); auto. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a1 a0)); intros Z0. rewrite <- (pluspf_inv3a_eq a1 a0 l2 l1); auto. case (ltT_dec A n ltM ltM_dec a1 a); [ intros H2; case H2; clear H2 | idtac ]; intros H2. cut (ltT ltM a0 a); [ intros Ord0 | apply eqT_compat_ltTl with (b := a1) ]; auto. rewrite <- (pluspf_inv2_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX a (pluspf (pluspf (pX a1 l2) (pX a0 l1)) l0)); auto. rewrite <- (pluspf_inv3a_eq a1 a0 l2 l1); auto. rewrite <- (pluspf_inv2_eqa a (pluspf l2 l1) l0); auto. apply order_pluspf; auto. apply canonical_skip_fst with (b := a1); auto. apply canonical_skip_fst with (b := a0); auto. apply eqpP1; auto. apply H' with (y := (pX a1 l2, (pX a0 l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. repeat rewrite (fun a b : nat => Nat.add_comm a (S b)); simpl in |- *. repeat rewrite (Nat.add_comm (size A n l1)); auto. cut (ltT ltM a a0); [ intros Ord0 | apply eqT_compat_ltTr with (b := a1) ]; auto. rewrite <- (pluspf_inv1_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv3a_eq a1 a0 l2 (pluspf l1 (pX a l0))); auto. apply H' with (y := (l2, (l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a0 a)); intros Z1. cut (eqT a0 a); [ intros eqTerm0 | apply (eqT_trans A n) with (y := a1); auto; apply (eqT_sym A n) ]; auto. cut (eqT a (plusTerm (A:=A) plusA (n:=n) a1 a0)); [ intros eqTerm1 | apply (eqT_trans A n) with (y := a0); auto; apply (eqT_sym A n); auto; apply (plusTerm_eqT2 A plusA n) ]; auto. cut (eqT (plusTerm (A:=A) plusA (n:=n) a a1) a0); [ intros eqTerm2 | apply (eqT_trans A n) with (y := a); [ apply (plusTerm_eqT1 A plusA n) | apply (eqT_trans A n) with (y := a1) ]; auto; apply (eqT_sym A n) ]; auto. cut (eqT (plusTerm (A:=A) plusA (n:=n) a1 a) a0); [ intros eqTerm3 | apply (eqT_trans A n) with (y := a); auto; [ apply (plusTerm_eqT2 A plusA n) | apply (eqT_sym A n) ] ]; auto. cut (eqT a1 (plusTerm (A:=A) plusA (n:=n) a a0)); [ intros eqTerm4 | apply (eqT_trans A n) with (y := a0); auto; apply (eqT_sym A n); apply (plusTerm_eqT2 A plusA n); auto; apply (eqT_sym A n) ]; auto. cut (eqT a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); [ intros eqTerm5 | apply (eqT_trans A n) with (y := a0); auto; apply (eqT_sym A n); apply (plusTerm_eqT1 A plusA n) ]; auto. rewrite <- (pluspf_inv3a_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv2_eqa a (pluspf l2 l1) l0); auto. rewrite <- (pluspf_inv1_eqa a1 l2 (pluspf l1 l0)); auto. apply eqpP1; auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a (plusTerm (A:=A) plusA (n:=n) a1 a0)); auto. apply zeroP_plusTermr with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a a0)); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a a1) a0); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply plusTerm_assoc with (1 := cs); auto. apply (eqT_sym A n); auto. apply (eqT_sym A n); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a) a0); auto. apply plusTerm_comp_l with (1 := cs); auto. apply plusTerm_com with (1 := cs); auto. apply (eqT_sym A n); auto. apply plusTerm_assoc with (1 := cs); auto. apply plusTerm_comp_r with (1 := cs); auto. apply plusTerm_com with (1 := cs); auto. apply (eqT_sym A n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply zeroP_plusTermr with (1 := cs); auto. apply H' with (y := (l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. apply order_pluspf; auto. apply canonical_pX_eqT with (a := a0); auto. apply (eqT_sym A n); auto. apply canonical_pX_eqT with (a := a); auto. apply (eqT_sym A n); auto. apply order_pluspf; auto. apply canonical_pX_eqT with (a := a1); auto. apply canonical_pX_eqT with (a := a0); auto. cut (eqT a0 a); [ intros Ord0 | apply (eqT_trans A n) with (y := a1); auto; apply (eqT_sym A n) ]; auto. cut (eqT a (plusTerm (A:=A) plusA (n:=n) a1 a0)); [ intros eqTerm1 | apply (eqT_trans A n) with (y := a0); auto; apply (eqT_sym A n); auto; apply (plusTerm_eqT2 A plusA n) ]; auto. rewrite <- (pluspf_inv3b_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv3b_eq a1 (plusTerm (A:=A) plusA (n:=n) a0 a) l2 (pluspf l1 l0)) ; auto. rewrite <- (pluspf_inv2_eqa a (pluspf l2 l1) l0); auto. apply eqpP1; auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a (plusTerm (A:=A) plusA (n:=n) a1 a0)); auto. apply zeroP_plusTermr with (1 := cs); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a); auto. apply plusTerm_com with (1 := cs); auto. apply plusTerm_assoc with (1 := cs); auto. apply (eqT_sym A n); auto. apply H' with (y := (l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. apply order_pluspf; auto. apply canonical_pX_eqT with (a := a1); auto. apply canonical_pX_eqT with (a := a0); auto. apply (eqT_trans A n) with (y := a); auto; apply (eqT_sym A n); auto. apply (plusTerm_eqT2 A plusA n); auto. red in |- *; intros H'3; absurd (zeroP (A:=A) A0 eqA (n:=n) a); auto. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply plusTerm_assoc with (1 := cs); auto. apply (eqT_sym A n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply zeroP_plusTerml with (1 := cs); auto. apply (eqT_sym A n); auto. rewrite <- (pluspf_inv3b_eq a1 a0 l2 l1); auto. case (ltT_dec A n ltM ltM_dec a0 a); [ intros H1; case H1; clear H1 | idtac ]; intros H1. cut (ltT ltM a1 a); [ intros Ord0 | apply eqT_compat_ltTl with (b := a0); auto; apply (eqT_sym A n) ]; auto. cut (ltT ltM (plusTerm (A:=A) plusA (n:=n) a1 a0) a); [ intros Ord1 | apply eqT_compat_ltTl with (b := a1); auto; apply (eqT_sym A n); apply (plusTerm_eqT1 A plusA n) ]; auto. rewrite <- (pluspf_inv2_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv2_eq a1 a l2 (pluspf (pX a0 l1) l0)); auto. rewrite <- (pluspf_inv2_eq (plusTerm (A:=A) plusA (n:=n) a1 a0) a (pluspf l2 l1) l0) ; auto. apply eqpP1; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (pluspf (pX a1 l2) (pX a0 l1)) l0); auto. rewrite <- (pluspf_inv3b_eq a1 a0 l2 l1); auto. apply H' with (y := (pX a1 l2, (pX a0 l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. repeat rewrite (fun a b : nat => Nat.add_comm a (S b)); simpl in |- *. repeat rewrite (Nat.add_comm (size A n l1)); auto. cut (ltT ltM a a1); [ intros Ord0 | apply eqT_compat_ltTr with (b := a0); auto; apply (eqT_sym A n) ]; auto. cut (ltT ltM a (plusTerm (A:=A) plusA (n:=n) a1 a0)); [ intros Ord1 | apply eqT_compat_ltTr with (b := a0); auto; apply (eqT_sym A n); apply (plusTerm_eqT2 A plusA n) ]; auto. rewrite <- (pluspf_inv1_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv3b_eq a1 a0 l2 (pluspf l1 (pX a l0))); auto. rewrite <- (pluspf_inv1_eq (plusTerm (A:=A) plusA (n:=n) a1 a0) a (pluspf l2 l1) l0) ; auto. apply eqpP1; auto. apply H' with (y := (l2, (l1, pX a l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. cut (eqT a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); [ intros eqTerm1 | apply (eqT_trans A n) with (y := a0); auto; apply (eqT_sym A n); apply (plusTerm_eqT1 A plusA n) ]; auto. cut (eqT a1 a); [ intros eqT0 | apply (eqT_trans A n) with (y := a0); auto; apply (eqT_sym A n) ]; auto. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a0 a)); intros Z1. rewrite <- (pluspf_inv3a_eq a0 a l1 l0); auto. rewrite <- (pluspf_inv1_eqa a1 l2 (pluspf l1 l0)); auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a)); [ intros Z2 | idtac ]. rewrite <- (pluspf_inv3b_eq (plusTerm (A:=A) plusA (n:=n) a1 a0) a (pluspf l2 l1) l0) ; auto. apply eqpP1; auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); auto. apply plusTerm_assoc with (1 := cs); auto. apply (eqT_sym A n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply zeroP_plusTermr with (1 := cs); auto. apply H' with (y := (l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. apply (eqT_trans A n) with (y := a1); auto. apply (plusTerm_eqT1 A plusA n); auto. red in |- *; intros H'3; absurd (zeroP (A:=A) A0 eqA (n:=n) a1); auto. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a0 a)); auto. apply plusTerm_assoc with (1 := cs); auto. apply (eqT_sym A n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply zeroP_plusTermr with (1 := cs); auto. apply order_pluspf; auto. apply canonical_pX_eqT with (a := a0); auto. apply (eqT_trans A n) with a; auto. apply (eqT_sym A n); auto. apply canonical_pX_eqT with (a := a); auto. apply (eqT_sym A n); auto. rewrite <- (pluspf_inv3b_eq a0 a l1 l0); auto. cut (eqTerm eqA (plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a) (plusTerm (A:=A) plusA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a0 a))); [ intros eqTerm0 | idtac ]. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a)); intros Z2. rewrite <- (pluspf_inv3a_eq (plusTerm (A:=A) plusA (n:=n) a1 a0) a (pluspf l2 l1) l0) ; auto. rewrite <- (pluspf_inv3a_eq a1 (plusTerm (A:=A) plusA (n:=n) a0 a) l2 (pluspf l1 l0)) ; auto. apply H' with (y := (l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a); auto. apply (eqT_trans A n) with (y := a0); auto. apply (plusTerm_eqT2 A plusA n); auto. rewrite <- (pluspf_inv3b_eq (plusTerm (A:=A) plusA (n:=n) a1 a0) a (pluspf l2 l1) l0) ; auto. rewrite <- (pluspf_inv3b_eq a1 (plusTerm (A:=A) plusA (n:=n) a0 a) l2 (pluspf l1 l0)) ; auto. apply eqpP1; auto. apply H' with (y := (l2, (l1, l0))); simpl in |- *; auto. red in |- *; red in |- *; simpl in |- *; auto with arith. apply nzeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) (plusTerm (A:=A) plusA (n:=n) a1 a0) a); auto. apply (eqT_trans A n) with (y := a0); auto. apply (plusTerm_eqT2 A plusA n); auto. apply plusTerm_assoc with (1 := cs); auto. apply (eqT_sym A n); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)