proposition: Lemma Vr_monomial n a e: Vr (Lg \1c (fun _ : Set => J n a)) e = Yo (e = n) a \0c.
proof: Proof. rewrite /Vr Lg_range funI_set1 /Vg range_set1;case:(equal_or_not e n) => en; Ytac0. set_extens t. by move/setU_P => [y ty /Zo_P [/set1_P <-]] . rewrite en;move=> ti; apply/setU_P; exists a => //; apply/Zo_P; fprops. apply/set0_P => u. by move => /setU_P [y yu /Zo_P[/set1_P -> ]] /set1_P /pr1_def. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)