proposition: Lemma ge0_muleDl x y z : 0 <= y -> 0 <= z -> (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 paddr_eq0 //; move: s0; rewrite lee_fin. case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e. + rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0. by case: ltgtP t0 => // [t0|[<-{t}]] _; [rewrite gt_eqF|rewrite eqxx]. + by move: t0; rewrite lee_fin; case: (ltgtP t). - by rewrite ltry; case: ltgtP s0. - by rewrite ltry; case: ltgtP t0. - by rewrite ltry. - rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin. case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e. + rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0. by case: ltgtP t0 => // [t0|[<-{t}]]. + by move: t0; rewrite lee_fin; case: (ltgtP t). - by rewrite ltry; case: ltgtP s0. - by rewrite ltry; case: ltgtP s0. - by rewrite ltry; case: ltgtP s0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed