proposition: Lemma beta_def x y z : β (cPair x y) z = rem y (S (x * S z)) (gtBeta _ _).
proof: Proof. unfold beta. now rewrite !cPairProjections2, !cPairProjections1. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)