The Coq mailing list

["Daniel Galvez" <dt.galvez AT gmail.com>]

Hello,

A subgoal in a proof of mine is the following:

forall n:nat, (1 # Pos.of_nat n) == (1 # (2*Pos.of_nat n)) + (1 # (2 *
Pos.of_nat n)).

That is, 1/n = 1/(2n) + 1/(2n).

The domain of discourse here is the rationals. Perhaps there is something I am
not seeing being new to Coq, but I would expect a simple call to some tactic
like compute to dismiss this. I make progress in the code below by doing
induction on n, but am at a complete as for what to do in the inductive case.

(Note that the edge case of n = 0 does not invalidate this, as Post.of_nat 0 =
1.)

Require Import QArith.

Theorem simple:
forall n:nat, (1 # Pos.of_nat n) == (1 # (2*Pos.of_nat n)) + (1 # (2 *
Pos.of_nat n)).
intros.
unfold Qplus.
unfold Qeq. simpl.
induction n.
simpl. reflexivity.

Does anyone have a suggestion as to where I should look for completing this
proof?

Thank you,
Daniel Galvez