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