proposition: Lemma bigjoinP r : bigjoin_spec r (\join_(i <- r) F i).
proof: Proof. elim: r => [|i r]; first by rewrite big_nil; constructor. rewrite big_cons; case=> [|j jr]. by case: r => // _; rewrite joinx0; constructor; rewrite mem_head. by case: lcomparableP (letot (F i) (F j)) => //= _ _; constructor; rewrite ?mem_head // in_cons jr orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)