proposition: Lemma cnode_mirror : (cnode : rel mirror) =2 (cnode : rel G).
proof: Proof. exact: same_fconnect_finv (@nodeI G). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)