proposition: Theorem degen_assoc: forall p1 p2 p3, (p1 = inf_elt \/ p2 = inf_elt \/ p3 = inf_elt) \/ (p1 = opp p2 \/ p2 = opp p3) \/ (opp p1 = add p2 p3 \/ opp p3 = add p1 p2) -> add p1 (add p2 p3) = add (add p1 p2) p3.
proof: Proof. intros p1 p2 p3; intuition; subst; repeat (rewrite add_opp || rewrite add_0_r || rewrite add_0_l); auto. repeat rewrite (add_comm (opp p2)). rewrite add_opp; rewrite (add_comm p2); rewrite add_minus_id; auto. pattern p3 at 4; rewrite <- opp_opp; rewrite add_minus_id. rewrite (add_comm (opp p3)); rewrite add_opp; rewrite add_0_r; auto. rewrite <- H0; rewrite add_opp. rewrite <- (opp_opp p1); rewrite H0. rewrite opp_add. rewrite (add_comm (opp p2)); pattern p2 at 2; rewrite <- opp_opp; rewrite add_minus_id. rewrite add_comm; auto; rewrite add_opp; auto. pattern p3 at 1; rewrite <- opp_opp; rewrite H0. rewrite (add_comm p2). pattern p2 at 2; rewrite <- opp_opp. rewrite opp_add; rewrite add_minus_id; auto. rewrite <- H0; rewrite (add_comm (opp p3)). repeat rewrite add_opp; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith