fact: Definition factZ_it_F (fact : Z -> Z) (x : Z) := match Z_lt_le_dec x 0 with left h => 0 | right h => match Z.eq_dec 0 x with left h' => 1 | right h'' => x * fact (x - 1) end end.
imports: ZArith ZArithRing Zcompare Zwf Lia