proposition: Lemma const0_eq n : const0 n = if n == 0 then 0 else const0 (n.-1).
proof: Proof. apply: (Fix_eq xpredT) => // {n} f g n _. rewrite /const0_rec. case: ifP => // /negbT. case: n => //= n _ Hfg. exact: Hfg. Qed.
imports: mathcomp(all_ssreflect)