proposition: Lemma clink_glink : connect clink =2 gcomp.
proof: Proof. move=> x; apply/subset_eqP/andP. split; apply/subsetP; apply: connect_sub x => x y. case/clinkP=> [-> | <-]; last by rewrite connect1 ?glinkF. by rewrite glinkC connect1 ?glinkN. case/predU1P=> [<- | /pred2P[<- | <-]]; last by rewrite connect1 ?clinkF. rewrite -{1}[x]edgeK (connect_trans (connect1 (clinkN _))) //. by rewrite clinkC connect1 ?clinkF. by rewrite clinkC connect1 ?clinkN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)