proposition: Theorem addeA p1 p2 p3 : adde p1 (adde p2 p3) = adde (adde p1 p2) p3.
proof: Proof. have [->|/eqP p1Dinf] := p1 =P inf_elt; first by apply/degen_assoc/Or31/Or31. have [->|/eqP p2Dinf] := p2 =P inf_elt; first by apply/degen_assoc/Or31/Or32. have [->|/eqP p3Dinf] := p3 =P inf_elt; first by apply/degen_assoc/Or31/Or33. have [->|/eqP p1Dp2] := p1 =P p2. by rewrite ![adde p2 _]addeC -spec4_assoc addeC. have [p1E|/eqP p1DNp2] := p1 =P oppe p2; first by apply/degen_assoc/Or32; left. have [->|/eqP p2Dp3] := p2 =P p3; first by apply: spec4_assoc. have [p2E|/eqP p2DNp3] := p2 =P oppe p3; first by apply/degen_assoc/Or32; right. have [Np1E|/eqP Np1Dp2Dp3] := oppe p1 =P adde p2 p3. by apply/degen_assoc/Or33; left. have [Np3E|/eqP Np3Dp1Dp2] := oppe p3 =P adde p1 p2. by apply/degen_assoc/Or33; right. have [->|/eqP p1Dp2Dp3] := p1 =P adde p2 p3. apply: addeI (_ : adde (oppe p3) _ = _). rewrite spec4_assoc ![adde (oppe p3) _]addeC. by rewrite !addeK addeC. have [->|/eqP p3Dp1Dp2] := p3 =P adde p1 p2. apply: addeI (_ : adde (oppe p1) _ = _). by rewrite spec4_assoc ![adde (oppe p1) _]addeC ![adde p1 _]addeC !addeK. apply: spec1_assoc. - apply/and4P; split => //. - apply/and4P; split => //. - apply/and4P; split => //. - apply/eqP => p1Dp2Dinf; case/eqP: p1DNp2. by apply: uniq_oppe; rewrite addeC. - by rewrite eq_sym. by rewrite eq_sym. apply/and4P; split => //. apply/eqP=> p2Dp3Dinf; case/eqP: p2DNp3; apply: uniq_oppe. by rewrite addeC. apply/eqP=> p1DNp2Dp3; case/eqP: Np1Dp2Dp3. by rewrite p1DNp2Dp3 oppeK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)