proposition: Lemma N2pos_lt_switch2 : forall n p, (0%N < n)%N -> ((N2pos n < p)%positive <-> (n < N.pos p)%N).
proof: Proof. intros n p H; N2pos_destruct n n; split; simpl;now rewrite pos2N_inj_lt. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)