proposition: Lemma Qpos_is_enumerator : IsSurjection@{UQ} Qpos_enumerator.
proof: Proof. apply BuildIsSurjection. unfold hfiber. intros e;generalize (@center _ (enumerator_issurj Q (' e))). apply (Trunc_ind _). intros [n E]. apply tr;exists n. unfold Qpos_enumerator. destruct (le_or_lt (enumerator Q n) 0) as [E1|E1]. - destruct (irreflexivity lt 0). apply lt_le_trans with (enumerator Q n);trivial. rewrite E;solve_propholds. - apply pos_eq,E. Qed.
imports: HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.sum HoTT.Classes.orders.dec_fields HoTT.Classes.orders.lattices HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac