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