proposition: Lemma clt_6: [/\ \0c <c \6c, \1c <c \6c, \2c <c \6c, \3c <c \6c & \4c <c \6c /\ \5c <c \6c].
proof: Proof. have hf:=(cltS NS5);move:clt_5 => [ha hb hc hd he]. move: (clt_ltT ha hf) (clt_ltT hb hf) (clt_ltT hc hf) => ra rb rc. move: (clt_ltT hd hf) (conj (clt_ltT he hf) hf)=> rd re. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)