proposition: Lemma NltP a: natp a -> forall x, x <c a <-> inc x a.
proof: Proof. move => aN x; split; first by move /oclt; apply: olt_i. move => xa. apply: (oclt3 (CS_nat (NS_inc_nat aN xa)) (CS_nat aN)). by apply/(oltP (OS_nat aN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)