proposition: Lemma le0_muleDl x y z : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x.
proof: Proof. rewrite /mule/=; move: x y z => [r| |] [s| |] [t| |] //= s0 t0. - by rewrite mulrDl. - by case: ltgtP => // -[] <-; rewrite mulr0 adde0. - by case: ltgtP => // -[] <-; rewrite mulr0 adde0. - by case: ltgtP => //; rewrite adde0. - rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin. case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e. + rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=. by rewrite !ltNge ltW //. + by case: (ltgtP t). - by rewrite ltry; case: ltgtP s0. - by rewrite ltry; case: ltgtP t0. - by rewrite ltry. - rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin. case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e. + rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=. by rewrite !ltNge ltW // -lee_fin t0; case: eqP. + by case: (ltgtP t). - by rewrite ltNge s0 /=; case: eqP. - by rewrite ltNge t0 /=; case: eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed