proposition: Lemma height_lt_size (h:Hydra) : height h < hsize h.
proof: Proof. induction h as [s]. induction s as [| h s']. - simpl; auto with arith. - cbn. Abort. End Bad. Lemma height_lt_size (h:Hydra) : height h < hsize h. Proof. induction h using Hydra_rect2 with (P0 := h_forall (fun h => height h < hsize h)). - destruct h as [ | h s']. + cbn; auto with arith. + cbn; destruct IHh as [H H0]; assert (H1: lheight s' <= lhsize s'). { clear H; induction s'. - cbn; auto with arith. - cbn; destruct (lheight s') as [ | n]. + cbn in H0; destruct H0; apply IHs' in H0 . red in H; transitivity (hsize h0); auto. auto with arith. + cbn in H0; destruct H0. apply IHs' in H0. clear IHs'. rewrite Nat.succ_max_distr; transitivity (S (height h0) + (S n)). lia. cbn; lia. } clear H0; cbn; destruct (lheight s'). * lia. * specialize (max_le_plus (height h) n); lia. - easy. - split;auto. Qed.
imports: Coq(Arith Lia) hydras(Hydra_Lemmas More_Arith)