proposition: Lemma dfun_asym x y : dfun_leq x y -> dfun_leq y x -> x = y.
proof: Proof. move=>H1 H2; apply: fext=>z; by apply: poset_asym; [apply: H1 | apply: H2]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)