proposition: Lemma compl_joins (J : Type) (r : seq J) (P : {pred J}) (F : J -> L) : ~` (\join_(j <- r | P j) F j) = \meet_(j <- r | P j) ~` F j.
proof: Proof. by elim/big_rec2: _=> [|i x y ? <-]; rewrite ?compl0 ?complU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)