proposition: Lemma positive_ext : ∀ (p q : positive), p.(pos) = q.(pos) → p = q.
proof: Proof. intros [p hp] [q hq] e. cbn in e. subst. f_equal. apply eq_irrelevance. Qed.
imports: Coq(Utf8 Lia) mathcomp(ssreflect eqtype ssrbool ssrnat) extructures(ord fset) Equations(Equations)