proposition: Lemma Exercise1_19d: without_gaps r -> (forall i, inc i (substrate r) -> (without_gaps (Vg g i) \/ (forall x y, inc x (substrate (Vg g i)) -> inc y (substrate (Vg g i)) -> ~ (glt (Vg g i) x y)))) -> without_gaps (order_sum r g).
proof: Proof. move => [_ q1 q2] wg. apply/Exercise1_19a=> //; split; fprops; last first. by move => i j /q2 h; constructor 1. move=> i u v isr luv; case: (wg _ isr) => // h. have p1:inc u (substrate (Vg g i)) by order_tac. have p2:inc v (substrate (Vg g i)) by order_tac. by case: (h _ _ p1 p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)