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