proposition: Lemma lt_max_1_2 : forall x1 y1 x2 y2 : nat, x1 < x2 -> y1 < y2 -> max x1 y1 < max x2 y2.
proof: Proof. intros x1 y1 x2 y2 H H0. unfold max in |- *. elim (sumbool_of_bool (leb x2 y2)). intro y. rewrite y. elim (leb x1 y1). assumption. apply lt_le_trans with (m := x2). assumption. apply leb_complete. assumption. intro y. rewrite y. elim (leb x1 y1). apply lt_trans with (m := y2). assumption. apply leb_complete_conv. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)