proposition: Lemma cge1P x: (\1c <=c x) <-> (\0c <c x).
proof: Proof. split; move=> le1;first exact:(clt_leT (clt_01) le1). by apply: (ocle3 CS1 (proj32_1 le1)); apply /oge1P; exact: (oclt le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)