proposition: Lemma order_le_cycle : order x <= size p.
proof: Proof. apply: leq_trans (card_size _); apply/subset_leq_card/subsetP=> y. by rewrite !(fconnect_cycle, inE) ?eqxx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)