proposition: Lemma itv_total_join3E i1 i2 i3 : i1 `|` i2 `|` i3 \in [:: i1 `|` i2; i1 `|` i3; i2 `|` i3].
proof: Proof. case: i1 i2 i3 => [b1l b1r] [b2l b2r] [b3l b3r]; rewrite !inE /eq_op /=. case: (leP b1l b2l); case: (leP b1l b3l); case: (leP b2l b3l); case: (leP b1r b2r); case: (leP b1r b3r); case: (leP b2r b3r); rewrite ?eqxx ?orbT //= => b23r b13r b12r b23l b13l b12l. - by case: leP b13r (le_trans b12r b23r). - by case: leP b13r (le_trans b12r b23r). - by case: leP b13l (le_trans b12l b23l). - by case: leP b13l (le_trans b12l b23l). - by case: leP b13l (le_trans b12l b23l). - by case: leP b13r (lt_trans b23r b12r). - by case: leP b13l (lt_trans b23l b12l). - by case: leP b13l (lt_trans b23l b12l). - by case: leP b13l (lt_trans b23l b12l). - by case: leP b13r (lt_trans b23r b12r). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)