page 1
1
A Lemma About Double Operation
We want to prove
(
M N : Nat )
2 * M = 2 * N
implies
M = N .
We take the following steps:
Quantifier elimination
introduces the new constant(s)
m, n : Nat
.
Implication elimination
assumes
2 * m = 2 * n
.
We
introduce the lemma
(
M : Nat ) div2(2 * M) = M.
Click
here
to see its proof.
We apply an operation
div2
to the both sides of the equation in the hypothesis:
2 * m = 2 * n
,
and get
m = n
.
We change the equation
m = n
to rewriting rule.
We show
m = n
by
reduction
.
And thus the main goal is proved.
Left
Up
Down
Right
This page was generated by Kumo on Tue Feb 13 19:36:12 PST 2001.