-1
$\begingroup$

Open Scope Z_scope. Require Import ZArith. Require Import Znumtheory.

intros a b c d [Hab Hac] [H1 H2]. unfold Z.divide in *. destruct H1 as [H3 H1]. destruct H2 as [H4 H2]. exists (c * H3 + b * H4). rewrite Z.mul_add_distr_r. rewrite <- Z.mul_assoc. rewrite H1. rewrite H2. rewrite Z.mul_assoc. rewrite Z.add_comm. assert (exists z : Z, a = z * a) as H_a. exists (H3 * d). rewrite H1. assert (exists z : Z, b = z * a) as H_b. exists (H4 * d). rewrite H2. rewrite H1.

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ This is not a good question as written. There is no question. Your code is not properly formatted with backticks. You don’t explain what you are stuck on, what you have tried, if this is homework, etc. Ask yourself if when you are an expert in two years if you would take the time to answer a “question” like this? $\endgroup$
    – Jason Rute
    May 16 at 12:42
  • $\begingroup$ Sorry about that, I fixed my post. It was rather I was confused at the step I am at and proceeding I am not sure what to do. I am rather new to COQ and I am trying to familiarize myself and it is really hard so I have had a really hard time solving proofs. $\endgroup$
    – deleted_user0972
    May 16 at 12:51
  • $\begingroup$ Just stop bombarding us, please. For this sort of thing you might be better off in some sort of beginner channel at Coq Zulip. $\endgroup$
    – Andrej Bauer
    May 16 at 13:08
  • $\begingroup$ Sorry about that... But thank you for that helpful recommendation beginner channel at Coq Zulip $\endgroup$
    – deleted_user0972
    May 16 at 13:16

0

Reset to default

Browse other questions tagged or ask your own question.