proposition: Lemma ord3P (P : 'I_3 -> Type) : P ord0 -> P ord1 -> P ord2 -> forall i : 'I_3, P i.
proof: Proof. have H (i j : 'I_3) : i == j -> P i -> P j by move/eqP->. move => P0 P1 P2 [[|[|[|//]]] Hi]. exact: H P0. exact: H P1. exact: H P2. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph set_tac)