proposition: Lemma maxset_cofix : maxset [pred X | F X == X] cofixset.
proof: Proof. rewrite maxminset setCK (@minset_eq _ _ [pred X | G X == X]) ?minset_fix//. by move=> X /=; rewrite (can2_eq setCK setCK). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)