proposition: Lemma tri_ine (a b c : F) : ((a != b) <= (c != b) + (a != c))%nat.
proof: Proof. case/boolP : (a == b) => ab //=. by case/boolP : (c == b) => cb //=; rewrite add0n (eqP cb) {cb} ab. 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