proposition: Lemma real_wlog_ler P : (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=> sP hP a b ha hb; wlog: a b ha hb / a <= b => [hwlog|]; last exact: hP. by case: (real_leP ha hb)=> [/hP //|/ltW hba]; apply/sP/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)