proposition: Lemma Exercise1_19c: ne_substrate r -> (forall i u, ~ (minimal (Vg g i) u)) -> (forall i, inc i (substrate r) -> without_gaps (Vg g i)) -> without_gaps (order_sum r g).
proof: Proof. move => [y yE] nm wg. apply /Exercise1_19a;split => //. + by right; move: (wg _ yE)=> [_ [a [b ab]] _]; exists y, a, b. + by move => i c z h _; apply: wg. + move=> i j ij; constructor 3; apply: nm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)