proposition: Lemma clt_4: [/\ \0c <c \4c, \1c <c \4c, \2c <c \4c & \3c <c \4c].
proof: Proof. by have hd:=(cltS NS3);move:clt_3 => [ha hb hc]; split => //; apply: clt_ltT hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)