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