proposition: Lemma phi_principalR a b: { c:T2 | [a, b] = phi zero c}.
proof: Proof. case az:(a==zero); last by exists [a,b]; rewrite /= T2lt0n az. rewrite (eqP az); case: b; first by exists zero. move => a' b' n' c'. case az1: (a'==zero). exists (cons a' b' n' c'). by rewrite /= (eqP az1) T2ltnn !andbF; case: (_ && _). case h: ((n' == 0) && (c' == zero)). move/andP:h => [/eqP -> /eqP ->]. by exists (cons a' b' 0 one); rewrite /phi !eqxx T2lt0n az1 /=. case h':( (n' == 0) && T2finite1 c'); last first. by exists (cons a' b' n' c');rewrite /= T2lt0n az1 h h' /=. move/andP:h' => [/eqP ->]; case c' => //. move => a1 b2 n2 c1 /= /and3P[/eqP -> /eqP -> /eqP ->]. by exists (cons a' b' 0 (\F(n2.+2))); rewrite /= T2lt0n az1 /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)