proposition: Theorem degen_assoc p1 p2 p3 : [\/ [\/ p1 = inf_elt, p2 = inf_elt | p3 = inf_elt], p1 = oppe p2 \/ p2 = oppe p3 | oppe p1 = adde p2 p3 \/ oppe p3 = adde p1 p2] -> adde p1 (adde p2 p3) = adde (adde p1 p2) p3.
proof: Proof. case=> [[->|->|->]|[->|->]|[Np1E|Np3E]]; rewrite ?(adde0, add0e, addeN) //. - rewrite ![adde (oppe p2) _]addeC addeN add0e. by rewrite [adde p2 _]addeC addeK. - rewrite -[X in _ = adde _ X]oppeK addeK. by rewrite [adde _ p3]addeC addeN adde0. rewrite -Np1E addeN -(oppeK p1) Np1E oppe_adde. rewrite [adde (oppe p2) _]addeC -[X in _ = adde (adde _ X) _]oppeK addeK. by rewrite addeC addeN. rewrite -[in LHS](oppeK p3) Np3E [adde p2 _]addeC. rewrite oppe_adde -[X in adde _ (adde _ X)]oppeK addeK addeN. by rewrite -(oppeK p3) Np3E addeN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)