proposition: Lemma nth_fgraph_ord T n (x0 : T) (i : 'I_n) f : nth x0 (fgraph f) i = f i.
proof: Proof. by rewrite -[i in RHS]enum_rankK -tnth_fgraph (tnth_nth x0) enum_rank_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)