fact: Definition Exercise1_20_prop r:= forall x y, glt r x y -> exists x' y', [/\ gle r x x', glt r x' y', gle r y' y & (forall z, ~ (glt r x' z /\ glt r z y'))].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)