proposition: Lemma muleDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z.
proof: Proof. rewrite /mule/=; move: x y z => [x| |] [y| |] [z| |] //= _; try (by case: ltgtP => // -[] <-; rewrite ?(mul0r,add0r,adde0)) || (by case: ltgtP => //; rewrite adde0). by rewrite mulrDr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed