proposition: Lemma ex1_res3 i: inc i L -> ex1_gij (J i i) = identity (ex1_Fl i).
proof: Proof. move => iL; rewrite /ex1_gij pr1_pair pr2_pair ex1_res0. apply:prl_restr_trivial. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)