proposition: Lemma cond_Zopp_mult : forall s u v, cond_Zopp s (u * v) = (cond_Zopp s u * v)%Z.
proof: Proof. intros s u v. case s. apply sym_eq. apply Zopp_mult_distr_l_reverse. apply refl_equal. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic