proposition: Lemma iso_eq_F0_F1_F2 : forall r s : {perm cube}, is_iso3 r -> is_iso3 s -> r F0 = s F0 -> r F1 = s F1 -> r F2 = s F2 -> r = s.
proof: Proof. move=> r s hr hs hrs0 hrs1 hrs2. have:= hrs0; have:= hrs1; have:= hrs2. have e23: F2 = s0 F3 by apply/eqP; rewrite permE /S0f (tnth_nth F0). have e14: F1 = s0 F4 by apply/eqP; rewrite permE /S0f (tnth_nth F0). have e05: F0 = s0 F5 by apply/eqP; rewrite permE /S0f (tnth_nth F0). rewrite e23 e14 e05; rewrite !hr !hs. move/perm_inj=> hrs3; move/perm_inj=> hrs4; move/perm_inj=> hrs5. by apply/eqP; rewrite eqperm /= hrs0 hrs1 hrs2 hrs3 hrs4 hrs5 !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)