proposition: Lemma fproperI A B C : (A `<` B `&` C) -> (A `<` B) && (A `<` C).
proof: Proof. move=> pAI; apply/andP. by split; apply: (fproper_sub_trans pAI); rewrite (fsubsetIl, fsubsetIr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)