proposition: Lemma fdist_take_dropE x : fdist_take_drop x = P (row_mx (\row_(_ < 1) x.1.1) (castmx (erefl 1%nat, @subnKC i n (ltnS' (ltn_ord i))) (row_mx x.1.2 x.2))).
proof: Proof. rewrite /fdist_take_drop fdistmapE /=. rewrite (eq_bigl (fun a : 'rV_n.+1 => (g a == x)%bool)) //. rewrite {1}(_ : x = g (row_mx (\row_(k<1) x.1.1) (castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx x.1.2 x.2)))); last first. move: x => /= -[[x11 x12] x2]. rewrite /g row_mx_row_ord0 /=; congr (_, _, _). apply/rowP => j; rewrite !mxE !castmxE /= cast_ord_id mxE esymK. have @k : 'I_n. by apply: (@Ordinal _ j); rewrite (leq_trans (ltn_ord j)) // -ltnS. rewrite (_ : lift _ _ = rshift 1%nat k); last first. by apply val_inj => /=; rewrite /bump leq0n. rewrite (@row_mxEr _ 1%nat 1%nat) // castmxE /= cast_ord_id. rewrite (_ : cast_ord _ k = lshift (n - i) j). by rewrite row_mxEl. exact: val_inj. apply/rowP => j; rewrite mxE castmxE /= cast_ord_id mxE esymK. have @k0 : 'I_n by apply: (@Ordinal _ (i + j)); rewrite -ltn_subRL. rewrite (_ : lift _ _ = rshift 1%nat k0); last first. apply val_inj => /=; by rewrite /bump leq0n. rewrite (@row_mxEr _ 1%nat 1%nat) castmxE /=. rewrite (_ : cast_ord _ _ = rshift i j); last exact: val_inj. by rewrite row_mxEr cast_ord_id. by rewrite (big_pred1_inj inj_g). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext