3
Lemma double_div2: forall n, div2 (double n) = n.
4
exact (fun n => let _subcase :=
5
let _cofact := fun _ : 0 = 0 => refl_equal 0 in
6
_cofact (let _fact := refl_equal 0 in _fact) in
8
fun (m : nat) (Hrec : div2 (double m) = m) =>
9
let _fact := f_equal div2 (double_S m) in
10
let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in
14
(f_equal (fun f : nat -> nat => f (div2 (double m)))
15
(refl_equal S)) (f_equal S Hrec)) in
17
(fix _fix (__ : nat) : div2 (double __) = __ :=
18
match __ as n return (div2 (double n) = n) with
21
(fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec)