proposition: Theorem spec4_assoc p1 p2 : adde p1 (adde p2 p2) = adde (adde p1 p2) p2.
proof: Proof. have [->|/eqP p1Dinf] := p1 =P inf_elt. by apply/degen_assoc/Or31/Or31. have [->|/eqP p2Dinf] := p2 =P inf_elt. by apply/degen_assoc/Or32; right. have [p2E|/eqP p2DNp2] := p2 =P oppe p2. by apply/degen_assoc/Or32; right. have [p1E|/eqP p1DNp2] := p1 =P oppe p2. by apply/degen_assoc/Or32; left. have [Np1E|/eqP Np1Dp2Dp2] := oppe p1 =P adde p2 p2. by apply/degen_assoc/Or33; left. have [Np2E|/eqP Np2Dp1Dp2] := oppe p2 =P adde p1 p2. by apply/degen_assoc/Or33; right. have [p1E|/eqP Np2Dp2Dp2] := p1 =P adde p2 p2. subst p1. apply: spec3_assoc. - apply/and4P; split => //. apply/eqP => p2Dp2Ep2; case/eqP : p2Dinf. by apply: uniq_zeroe (_ : _ = p2). - by apply/and3P; split. - apply/and4P; split => //. - apply/eqP => p2Dp2Dp2Einf; case/eqP : p1DNp2. by apply: uniq_oppe; rewrite addeC. - apply/eqP => p2Dp2Dp2Ep2; case/eqP : p1Dinf. by apply: uniq_zeroe (_ : _ p2). by rewrite eq_sym. apply/and3P; split => //. by rewrite eq_sym. have [p2E|/eqP p2Dp1Dp2] := p2 =P adde p1 p2. rewrite [in LHS](uniq_zeroe (sym_equal p2E)). by rewrite -p2E. have [->|/eqP p1Dp2] := p1 =P p2; first by rewrite addeC. apply: spec2_assoc. - by apply/and4P; split. - by apply/and3P; split. - apply/and4P; split => //. - apply/eqP => p1Dp2Einf; case/eqP: p1DNp2. by apply: uniq_oppe; rewrite addeC. - by rewrite eq_sym. by rewrite eq_sym. apply/and4P; split => //. apply/eqP => p2Dp2Einf; case/eqP: p2DNp2. by apply: uniq_oppe. apply/eqP => p1DNp2p2; case/eqP: Np1Dp2Dp2. by rewrite p1DNp2p2 oppeK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)