proposition: Lemma a_very_specific_lemma3 : forall (a b c d : Z) (s r t u : positive), (a * r)%Z = (b * s)%Z -> (c * u)%Z = (d * t)%Z -> ((a * t + c * s) * (r * u)%positive)%Z = ((b * u + d * r) * (s * t)%positive)%Z.
proof: Proof. intros a b c d s r t u. intros. change (((a * t + c * s) * (r * u))%Z = ((b * u + d * r) * (s * t))%Z) in |- *. apply a_very_specific_lemma2; trivial. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid