Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
29 lines (22 sloc) 533 Bytes
module parity
data Parity : Nat -> Set where
even : Parity (n + n)
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
parity_lemma_2 = proof {
intro;
intro;
rewrite sym (plusSuccRightSucc j j);
trivial;
}
parity_lemma_1 = proof {
intro j;
intro;
rewrite sym (plusSuccRightSucc j j);
trivial;
}
Jump to Line
Something went wrong with that request. Please try again.