proposition: Lemma Exercise6_12a n: natp n -> n <> \0c -> (inc \1c (Nint1c n) /\ inc n (Nint1c n)).
proof: Proof. move => nN nz; split; apply/(Nint1cP nN); split; fprops. apply /cge1P;apply: card_ne0_pos => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)