proposition: Lemma clt_3: [/\ \0c <c \3c, \1c <c \3c & \2c <c \3c].
proof: Proof. have ha:=(cltS NS2). split; [ exact: (clt_ltT clt_02 ha) | exact: (clt_ltT clt_12 ha) | exact: ha]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)