proposition: Lemma sphere_not_empty n (F : finRingType) r (rn : r <= n) (x : 'rV[F]_n) : [set y | dH x y == r] != set0.
proof: Proof. destruct r as [|r']. rewrite /dH. apply/negP => /eqP/setP/(_ x). by rewrite inE subrr wH0 eqxx !inE. set r := r'.+1. apply/set0Pn. set y : 'rV[F]_n:= (\row_i if i < r then 1 else 0)%R. exists (x + y)%R. rewrite inE dH_wH. rewrite (_ : y = castmx (erefl, subnKC rn) (@row_mx _ 1 r (n -r) (const_mx 1%R) 0)). by rewrite wH_castmx wH_row_mx. apply/rowP => i. rewrite !castmxE /= cast_ord_id /= mxE. case: ifPn => ir; set j := cast_ord _ _. rewrite (_ : j = lshift _ (Ordinal ir)); last by apply val_inj. by rewrite row_mxEl mxE. have ir' : i - r < n - r. rewrite subnS prednK //; last first. rewrite subn_gt0; move: ir; by rewrite -leqNgt. destruct n as [|n'] => //. rewrite subSS leq_sub2r //; by move: (ltn_ord i). rewrite (_ : j = rshift _ (Ordinal ir')); last first. apply val_inj => /=; by rewrite subnKC // leqNgt. by rewrite row_mxEr mxE. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext