proposition: Lemma adde_maxr : right_distributive (@GRing.add (\bar R)) maxe.
proof: Proof. move=> x y z; have [yz|zy] := leP y z. by apply/esym/max_idPr; rewrite leeD2l. by apply/esym/max_idPl; rewrite leeD2l// ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed