coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Stuck on a proof of div2 (n + n) = n.

From: frank maltman <frank.maltman AT googlemail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Stuck on a proof of div2 (n + n) = n.
Date: Sat, 21 May 2011 11:12:31 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:x-mailer:mime-version:content-type :content-transfer-encoding; b=IIrAOprQoK4oBfA6U9GvkSClxojtBqBLUiv8v081BRvrO6Gr/zjf8fxHfah/1c8RNC P7yfW+Z1pj0K8SEFmb/jH+8rYNwhhFwtwnAW/Twu7BOcfIxUx6GwLa6ckaSc2/KoVlCk OpX4702q3x3oHTv0gEHFO6pkuAK2h6gm2X/NY=

Hello.

As the subject states, I'm trying to prove the following lemma:

  Lemma divplus : forall n, div2 (n + n) = n.

The furthest I've managed to get with this is:

induction n using ind_0_1_SS.
reflexivity.
reflexivity.
simpl.
apply eq_S.

Which leaves me at the following subgoal:

  n : nat
  IHn : div2 (n + n) = n
  ============================
   div2 (n + S (S n)) = S n

I'm unable to go further. Is there some obvious mistake
in my approach?

[Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
- Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Chris Dams
  - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
    - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
      - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., julien forest
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
      - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Pierre Casteran
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Pierre Casteran
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman