proposition: Lemma dH_tri_ine n (c a b : 'rV[F]_n) : (@dH _ n a b <= dH a c + dH c b)%nat.
proof: Proof. elim: n a b c => [a b c|n IH a b c]. by rewrite (empty_rV a) (empty_rV b) (empty_rV c) /dH subrr wH0. rewrite /dH /wH. have H : forall v w : 'rV[F]_n.+1, count (fun x : F => x != 0) (tuple_of_row (v - w)) = addn (v ``_ 0 - w ``_ 0 != 0) (count (fun x => x != 0) (behead (tuple_of_row (v - w)))). move=> v w. rewrite (tuple_eta (tuple_of_row (v - w))) /=. by rewrite /tuple_of_row /thead tnth_map !mxE tnth_ord_tuple. rewrite !H {H} addnCA !addnA -addnA leq_add //; last first. move: {IH}(IH (row_of_tuple [tuple of (behead (tuple_of_row a))]) (row_of_tuple [tuple of (behead (tuple_of_row b))]) (row_of_tuple [tuple of (behead (tuple_of_row c))])). rewrite /dH /wH. set lhs := (X in (X <= _)%nat -> _). set rhs := (X in (_ <= X)%nat -> _) => IH. apply (@leq_trans lhs). rewrite /lhs. apply eq_leq. rewrite (_ : tuple_of_row _ = [tuple of (behead (tuple_of_row (a - b)))]) //. apply eq_from_tnth. rewrite /tuple_of_row => i; by rewrite !(tnth_behead,tnth_mktuple,mxE). apply (leq_trans IH) => {IH}. rewrite leq_add //. - apply eq_leq. rewrite (_ : tuple_of_row _ = [tuple of (behead (tuple_of_row (a - c)))]) //. apply eq_from_tnth. rewrite /tuple_of_row => i; by rewrite !(tnth_behead,tnth_mktuple,mxE). - apply eq_leq. rewrite (_ : tuple_of_row _ = [tuple of (behead (tuple_of_row (c - b)))]) //. apply eq_from_tnth. rewrite /tuple_of_row => i; by rewrite !(tnth_behead,tnth_mktuple,mxE). by rewrite !subr_eq0 tri_ine. 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