proposition: Lemma tarski_gfp_greatest f : forall x : T, f x = x -> x <== tarski_gfp f.
proof: Proof. by move=>x H; apply: supP; rewrite InE /= H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)