Parameter D : Set. Axiom D_not_empty : exists d:D, True. Parameter lt : D -> D -> Prop. Parameter max : D -> D -> D. Notation "x < y" := (lt x y). Axiom lt_irreflexive : forall d : D, ~ d < d. Axiom lt_transitive : forall d d' d'' : D, d < d' -> d' < d'' -> d < d''. Axiom lt_cases : forall d d' : D, d < d' \/ d = d' \/ d' < d. Axiom D_not_bounded : forall x : D, exists y : D, x < y. Definition le x y := lt x y \/ x = y. Notation "x <= y" := (le x y). Axiom max_1 : forall x y : D, x <= max x y. Axiom max_2 : forall x y : D, y <= max x y. Axiom max_3 : forall x y m : D, x <= m -> y <= m -> max x y <= m. Theorem lt_not_gt : forall x y: D, x < y -> ~ y < x. Proof. intros x y H0 H1. absurd (x < x). apply lt_irreflexive. apply lt_transitive with (d':= y). assumption. assumption. Qed. Theorem le_reflexive : forall d : D, d <= d. Proof. intro d. unfold le. right. reflexivity. Qed. Theorem le_transitive : forall x y z : D, x <= y -> y <= z -> x <= z. Proof. unfold le. intros x y z H0 H1. destruct H0 as [H2 | H3]. left. destruct H1 as [H4 | H5]. apply lt_transitive with y. assumption. assumption. rewrite H5 in H2. assumption. rewrite H3. assumption. Qed. Theorem le_antisym : forall x y : D, x <= y -> y <= x -> x = y. Proof. unfold le. intros x y H0 H1. destruct H0 as [H2 | H3]. destruct H1 as [H4 | H5]. destruct (lt_not_gt x y H2). assumption. rewrite H5. reflexivity. assumption. Qed. Theorem le_lt_trans : forall x y z : D, x <= y -> y < z -> x < z. Proof. unfold le. intros x y z H0 H1. destruct H0 as [H2 | H3]. apply lt_transitive with y. assumption. assumption. rewrite H3. assumption. Admitted. Theorem lt_le_trans : forall x y z : D, x < y -> y <= z -> x < z. Proof. unfold le. intros x y z H0 H1. destruct H1 as [H2 | H3]. apply lt_transitive with y. assumption. assumption. rewrite H3 in H0. assumption. Qed. Theorem le_not_gt : forall x y : D, x <= y -> ~ y < x. Proof. unfold le. intros x y H0 H1. destruct H0 as [H2 | H3]. destruct (lt_not_gt x y H2). assumption. rewrite H3 in H1. destruct (lt_irreflexive y). assumption. Qed. Theorem max_eq : forall x : D, max x x = x. Proof. intro x. apply le_antisym. apply (max_3 x x x). apply le_reflexive. apply le_reflexive. apply (max_1 x x). Qed. Hint Resolve max_1 max_2 max_3 le_reflexive le_antisym le_transitive lt_transitive lt_irreflexive le_not_gt lt_not_gt lt_le_trans le_lt_trans. Theorem le_total : forall x y : D, x <= y \/ y <= x. Proof. intros x y. unfold le. destruct (lt_cases x y) as [H0 | [H1 | H2]]. left. left. assumption. left. right. assumption. right. left. assumption. Qed. Theorem max_comm : forall x y : D, max x y = max y x. Proof. intros x y. apply (le_antisym (max x y) (max y x) (max_3 x y (max y x) (max_2 y x) (max_1 y x)) (max_3 y x (max x y) (max_2 x y) (max_1 x y))). Qed. Theorem le_max : forall x y : D, x <= y -> max x y = y. Proof. intros x y H0. apply (le_antisym (max x y) y (max_3 x y y H0 (le_reflexive y)) (max_2 x y)). Qed. Theorem ge_max : forall x y : D, y <= x -> max x y = x. Proof. intros x y H0. rewrite (max_comm x y). apply (le_max y x). assumption. Qed. Hint Resolve le_max ge_max. Theorem max_or : forall x y : D, max x y = x \/ max x y = y. Proof. intros x y. destruct (le_total x y) as [H0 | H1]. right. apply (le_max x y). assumption. left. apply (ge_max x y). assumption. Qed. Theorem max_le : forall x y : D, max x y = y -> x <= y. Proof. intros x y H0. symmetry in H0. rewrite H0. apply (max_1 x y). Qed. Theorem max_ge : forall x y : D, max x y = x -> y <= x. Proof. intros x y H0. symmetry in H0. rewrite H0. apply (max_2 x y). Qed. Theorem max_assoc : forall x y z : D, max x (max y z) = max (max x y) z. Proof. intros x y z. rewrite (max_comm x y). rewrite (max_comm (max y x) z). assert (H0 : forall a b c : D, max a (max b c) <= max c (max b a)). intros a b c. destruct (le_total a (max b c)) as [H1 | H2]. rewrite (le_max a (max b c) H1). apply max_3. apply le_transitive with (max b a). apply max_1. apply max_2. apply max_1. rewrite (ge_max a (max b c) H2). apply le_transitive with (max b a). apply max_2. apply max_2. apply le_antisym. apply (H0 x y z). apply (H0 z y x). Qed. Section Top_absurd. Variable top: D. Hypothesis top_top : forall d : D, d <= top. Lemma super_top : exists x : D, top < x. Proof. apply (D_not_bounded top). Qed. Lemma no_top : False. Proof. destruct super_top as (x, H0). assert (H1 : x <= top). apply (top_top x). destruct (le_not_gt x top H1). assumption. Qed. End Top_absurd. Check no_top. Lemma pas_d_element_absorbant_pour_max : ~ exists e : D, forall x : D, max e x = e. Proof. intro H0. destruct H0 as (e, H1). destruct (D_not_bounded e) as (x, H2). destruct (max_ge e x (H1 x)) as [H3 | H4]. destruct (lt_not_gt x e H3). assumption. rewrite H4 in H2. destruct (lt_irreflexive e). assumption. Qed.