proposition: Lemma phi_inv2 a b a' b': phi a b = phi a' b' -> b < phi a b -> b' < phi a' b' -> b = b'.
proof: Proof. move => sa sb sc. move: (phi_inv0 sa sb sc) => aa. have sd: phi a b = [a, b] \/ phi a b = [a, T2pred b] /\ b = T2succ (T2pred b). case: (phi_cases a b); last by right. case => h; [by move: sb; rewrite h T2ltnn | by left]. have se: phi a b = [a, b'] \/ phi a b = [a, T2pred b'] /\ b' = T2succ (T2pred b'). rewrite sa aa; case: (phi_cases a' b'); last by right. case => h; [by move: sc; rewrite h T2ltnn | by left]. case sd; case se. + by move => ->; case => ->. + move => [ta tb] tc. move: (ta); rewrite tc; case => td; rewrite - td in tb. move: sa; rewrite tb - aa tc => h. symmetry in h; move: (phi_inv1 h) => [n [pa pb]]. move: tc; rewrite pa /= pb; case n => //=. move => hh. by move: (T2lt_psi_b a [T2_pr1 b, T2_pr2 b]); rewrite - hh T2ltnn. move => n' /=; case; case n' => //n'' /=; case => hb. by move: (n_Sn n''); rewrite - hb. + move =>tc [ta tb]. move: (ta); rewrite tc; case => td; rewrite - td in tb. have h:phi a (T2succ b') = [a, b'] by rewrite - tb. move: (phi_inv1 h) => [n [pa pb]]. move: tc; rewrite sa - aa pa /= pb; case n => //=. move => hh. by move: (T2lt_psi_b a [T2_pr1 b', T2_pr2 b']); rewrite - hh T2ltnn. move => n' /=; case; case n' => //n'' /=; case => hb. by move: (n_Sn n''); rewrite - hb. + by move => [-> u1] [v1 ->]; rewrite u1; move: v1; case => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)