proposition: Remark maxLemma : forall a b c d : nat, a <= b -> c <= d -> Nat.max a c <= Nat.max b d.
proof: Proof. lia. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)