proposition: Remark maxApp : forall a b : list nat, {fold_right Nat.max 0 (a ++ b) = fold_right Nat.max 0 a} + {fold_right Nat.max 0 (a ++ b) = fold_right Nat.max 0 b}.
proof: Proof. intros a b; induction a as [| a a0 Hreca]. - simpl; now right. - simpl. induction (Nat.max_dec a (fold_right max 0 (a0 ++ b))) as [a1 | b0]. + rewrite a1; left; symmetry. apply Nat.max_l. apply Nat.le_trans with (max a (fold_right max 0 (a0 ++ b))). * apply Nat.le_trans with (max a (fold_right max 0 a0)). -- apply Nat.le_max_r. -- apply maxLemma. ++ apply le_n. ++ apply maxLemma2. * rewrite a1; apply le_n. + induction Hreca as [a1| b1]. * rewrite a1; now left. * rewrite b0, b1; now right. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)