proposition: Lemma urankA_uniq x: uniqueness (urankA_prop x).
proof: Proof. move => a b [oa pa pb][ob pc pd]. case: (oleT_ell oa ob) => //; [ by move /pd | by move /pb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)