fact: Fixpoint number_of_pals_____OUT (f : nat -> nat) domain x := match domain with | O => 0 | S domain => (if eq_nat_dec (f domain) (f x) then 1 else 0) + number_of_pals_____OUT f domain x end.
imports: ZArith Lia MyNat