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