proposition: Lemma induct_height_max2 : forall n1 n2 : nat, exists n, n1 < n /\ n2 < n.
proof: Proof. Proof using. intros. destruct (lt_dec n1 n2). exists (S n2). lia. exists (S n1). lia. Qed.
imports: Coq.Lists.List Coq.Logic.ProofIrrelevance Coq.Program.Equality Coq.Arith.Compare_dec Coq.micromega.Lia