proposition: Lemma phi_cases a b: {phi a b = b} + {phi a b = [a, b]} + { phi a b = [a, T2pred b] /\ b = T2succ (T2pred b) }.
proof: Proof. case b; first by left; right. move => a' b' n' c' /=. case sa: (_ && _). case sb: (a < a'); [ by left; left | by left; right]. case sb: (_ && _); [right | by left; right]. move /andP: sb sa=> [/andP [/eqP -> h1]]. case sb:([a', b'] == one); first by case:(eqP sb) => ->; rewrite T2ltn0. simpl; rewrite sb => _; move: h1; case c' => //. move => a1 b1 n1 c1 /= /and3P [/eqP -> /eqP -> /eqP ->]. by split => //=;case n1 => //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)