proposition: Fact leperm_refl s : s <=R s.
proof: Proof. by apply/lepermP; exists 1; rewrite ?mulg1 // length1 addn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype