proposition: Lemma positive_eqP : Equality.axiom positive_eq.
proof: Proof. intros [n hn] [m hm]. unfold positive_eq. simpl. destruct (n == m) eqn:e. - move: e => /eqP e. subst. left. f_equal. apply eq_irrelevance. - move: e => /eqP e. right. intro h. apply e. inversion h. reflexivity. Qed.
imports: Coq(Utf8 Lia) mathcomp(ssreflect eqtype ssrbool ssrnat) extructures(ord fset) Equations(Equations)