proposition: Lemma val_compare: [/\ val_eq <> val_in, val_eq <> val_or, val_eq <> val_not, val_eq <> val_ex & [/\ val_in <> val_or, val_in <> val_not, val_in <> val_ex & [/\ val_or <> val_not, val_or <> val_ex & val_not <> val_ex]]].
proof: Proof. have ha:= clt_01. have hb:= clt_12. move: (cltS NS2); rewrite -/card_three => hc. move: (cltS NS3); rewrite -/card_four => hd. move:(clt_ltT ha hb)(clt_ltT hb hc)(clt_ltT hc hd) => he hf hg. move:(clt_ltT he hc)(clt_ltT hf hd)(clt_ltT he hg). move: ha hb hc hd he hf hg => [_ ha] [_ hb] [_ hc] [_ hd] [_ he] [_ hf] [_ hg] [_ hi] [_ hj] [_ hk]. split => //; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)