proposition: Lemma dH_tri_ine : forall n a b c, size a = n -> size b = n -> size c = n -> dH a b <= dH a c + dH c b.
proof: Proof. elim => [ [] // [] // [] // |]. move=> n IH [|ha ta] // [|hb tb] // [|hc tc] // [Ha] [Hb] [Hc]. rewrite /dH /= -/(dH ta tb) -/(dH ta tc) -/(dH tc tb). move: {IH}(IH _ _ _ Ha Hb Hc) => IH. apply: leq_trans. - apply leq_add; [by apply leqnn | by apply IH]. - rewrite !eqb_id !addnA -(addnC (hc (+) hb)) addnA -2!addnA; apply leq_add. + rewrite addnC; by apply addb_tri_ine. + by apply leqnn. 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