proposition: Lemma T3le_consE a b c n d a' b' c' n' d' : cons a b c n d <= cons a' b' c' n' d' = if ([a, b, c] < [a', b', c']) then true else if ([a, b, c] == [a', b', c']) then if (n < n')%N then true else if (n == n') then (d <= d') else false else false.
proof: Proof. rewrite /T3le T3lt_consE; case: (T3ltgtP [a, b, c] [a', b', c']) => //. + by rewrite orbT. + move => h; rewrite orbF; apply /negP => /eqP h'. by move: h; case : h' => -> -> ->; rewrite T3ltnn. + case => -> -> ->; case (ltngtP n n'); rewrite ?orbF ? orbT //. move => nn; apply /negP => /eqP h'. by move: nn; case : h' => ->; rewrite ltnn. by move => ->; rewrite T3eqE !eqxx /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)