proposition: Lemma cpred_pr0 a b: \0c <c a -> a <=c b -> natp b -> cpred a <c b.
proof: Proof. move => ra rb nN. move:(cpred_pr (NS_le_nat rb nN) (nesym (proj2 ra))) => [sa sb]. apply /(cleSlt0P (CS_nat sa) nN); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)