proposition: Lemma rV_of_natD_neq0 i j : i <> j -> i <> O -> j <> O -> (i < expn 2 n)%nat -> (j < expn 2 n)%nat -> rV_of_nat n i + rV_of_nat n j <> 0.
proof: Proof. move=> Hij Hi Hj Hin Hjn. destruct i => //. destruct j => //. contradict Hij. apply F2_addmx0 in Hij. have [ii Hii] : exists ii, i.+1 = nat_of_pos ii. exists (BinPos.P_of_succ_nat i). by rewrite -Pnat.nat_of_P_o_P_of_succ_nat_eq_succ BinPos_nat_of_P_nat_of_pos. have [jj Hjj] : exists jj, j.+1 = nat_of_pos jj. exists (BinPos.P_of_succ_nat j). by rewrite -Pnat.nat_of_P_o_P_of_succ_nat_eq_succ BinPos_nat_of_P_nat_of_pos. rewrite Hii Hjj in Hij. apply rV_of_nat_inj in Hij; last 2 first. by rewrite -Hii. by rewrite -Hjj. apply nat_of_pos_inj in Hij. rewrite Hjj; by subst ii. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext mathcomp(bigop zmodp ssralg matrix) ssralg_ext f2