proposition: Lemma sum_roots_order (T : finType) (f : T -> T) (inj_f : injective f) : #|T| = \sum_(x in froots f) order f x.
proof: Proof. exact/sum_rootsT/fconnect_sym. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)