proposition: Lemma pow3Monotone : forall a b : nat, a <= b -> pow3 a <= pow3 b.
proof: Proof. intros a b H; induction b as [| b Hrecb]. - simpl; replace a with 0 by lia. apply le_n. - simpl; rewrite Nat.lt_eq_cases in H; case H. + intro H0; apply Nat.le_trans with (pow3 b). * apply Hrecb; now apply Compat815.lt_n_Sm_le. * apply Nat.le_add_r. + intro H0; rewrite H0; apply le_n. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)