proposition: Lemma mutually_disjoint_prop2 x f: (forall i j y, inc i x -> inc j x -> inc y (f i) -> inc y (f j) -> i = j) -> mutually_disjoint (Lg x f).
proof: Proof. move=> hyp; apply: mutually_disjoint_prop; aw => i j y ix jy. by rewrite !LgV //; apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)