proposition: Lemma real_wlog_ltr P : (forall a, P a a) -> (forall a b, (P b a -> P a b)) -> (forall a b, a < b -> P a b) -> forall a b : R, a \is real -> b \is real -> P a b.
proof: Proof. move=> rP sP hP; apply: real_wlog_ler=> // a b. by rewrite le_eqVlt; case: eqVneq => [->|] //= _ /hP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)