proposition: Lemma ex6_res2 i j: gle rL i j -> function_prop (ex6_gij (J i j)) (ex6_Fl i) (ex6_Fl j).
proof: Proof. move => H. rewrite ex6_gij_prop1 (ex6_res1 H). exact:(inl_restr_cf_compat2 (ex6_prop5c H)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)