proposition: Lemma PminusN_le : forall x y:positive, x <= y -> Z_of_N (PminusN y x) = y - x.
proof: Proof. intros x y Hle;unfold PminusN. assert (H := Pminus_mask_spec y x);destruct (Pminus_mask y x). rewrite H;unfold Z_of_N;auto with zarith. rewrite H;unfold Z_of_N;auto with zarith. exfalso;lia. Qed.
imports: ZArith Lia