proposition: Lemma add_simpl3 x y: y != zero -> x + x * (T1omega * y) = x * (T1omega * y).
proof: Proof. case: x => // a n b;case y => // a' n' b' _; rewrite T1mul_omega. have e1: (one == zero) = false by done. have e2: (one + a' == zero) = false by rewrite T1add_eq0 e1. have e3: a < a + one by rewrite - succ_is_add_one succ_lt. have e4: a < a + (one + a') by apply: add_le4; rewrite e2. by case: eqP; rewrite /T1mul ? e1 ? e2 andbF -/T1mul {1}/T1add ? e3 ? e4. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)