proposition: Lemma cpring_def p : (if p is x :: _ then x = node x0 else False) -> ufcycle node (rev p) -> cpring = p.
proof: Proof. case Dp: {1}p => // [x p'] Dx /andP[cycNp Up]; rewrite {x}Dx in Dp. have{Up} Dn: size (rev p) = order node (node (node x0)). have p_nx0: node x0 \in rev p by rewrite mem_rev Dp mem_head. by rewrite (order_cycle cycNp Up) // -(fconnect_cycle cycNp p_nx0) fconnect1. rewrite (cycle_path x0) {1}Dp rev_cons last_rcons in cycNp. case/fpathP: cycNp => n Dp'; rewrite Dp' size_traject in Dn. by rewrite /cpring /orbit -Dn -Dp' revK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)