proposition: Lemma ltc0_add x y : ltc 0 x -> ltc 0 y -> ltc 0 (x + y).
proof: Proof. move: x y => [a b] [c d] /= /andP [/eqP-> ha] /andP [/eqP-> hc]. by rewrite addr0 eqxx addr_gt0. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)