proposition: Fact infperm_is_meet x y z : (x <=R infperm y z) = (x <=R y) && (x <=R z).
proof: Proof. rewrite /infperm -![x <=R _]leperm_maxpermMl. by rewrite mulgA -{1}maxpermV mulVg mul1g supperm_is_join. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype