proposition: Lemma ex1_res2 i j: gle rL i j -> function_prop (ex1_gij (J i j)) (ex1_Fl j) (ex1_Fl i).
proof: Proof. move =>/ex1_prop7/lf_function ff; rewrite/ex1_gij; saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)