proposition: Lemma lub_absorbs_conv (x y : L) p : x [+] y = x [+] y [+] x <|p|> y.
proof: Proof. have H : x [+] y = (x [+] y [+] x <|p|> y) [+] y <|p|> x. rewrite -[in LHS](convmm p (x [+] y)) lubDl 2!lubDr 2!convmm lubCA lubC. by rewrite (lubAC x). rewrite {1}H. have {2}<- : x [+] y [+] (x [+] y [+] x <|p|> y) = x [+] y [+] x <|p|> y by rewrite lubA lubxx. rewrite [in RHS]lubC. have <- : x [+] y [+] x <|p|> y [+] (x [+] y [+] x <|p|> y [+] y <|p|> x) = x [+] y [+] x <|p|> y [+] y <|p|> x by rewrite lubA lubxx. by rewrite -H. Qed.
imports: HB(structures) Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets Rstruct reals) mathcomp(finmap) Reals_ext realType_ext classical_sets_ext ssrR fdist fsdist convex