proposition: Lemma phi_inv0 a b a' b': phi a b = phi a' b' -> b < phi a b -> b' < phi a' b' -> a = a'.
proof: Proof. move => sa sb sc. have ->: a = T2_pr1 (phi a b). case: (phi_cases a b); last by move => [] ->. case => h; [by move: sb; rewrite h T2ltnn | by rewrite h]. have ->: a' = T2_pr1 (phi a' b'). case: (phi_cases a' b'); last by move => [] ->. case => h; [by move: sc; rewrite h T2ltnn | by rewrite h]. by rewrite sa. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)