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