proposition: Lemma connect_to_C1r x y z : ~~ z -[]-> y -> x -[]-> y -> x -[predC1 z]-> y.
proof: Proof. move=> Hzy Hxy. apply: connect_to_forced => //= z1 H1 H2 H3. by apply/eqP=> H4; case/negP: Hzy; rewrite -H4. Qed.
imports: mathcomp(all_ssreflect) extra