proposition: Theorem le_lt_or_eq : forall a b:A, le a b -> lt a b \/ a = b.
proof: Proof. Proof (fun a b Hle => proj1 (Nat.lt_eq_cases _ _) Hle). Definition lt_eq_lt_dec : forall a b:A, {lt a b} + {a = b} + {lt b a} := lt_eq_lt_dec. End Nat_Order. Definition bool_le (b b':bool) := if b then if b' then True else False else True. Definition bool_lt (b b':bool) := if b then False else if b' then True else False. Module Bool_Order : DEC_ORDER with Definition A := bool with Definition le := bool_le with Definition lt := bool_lt. Definition A := bool. Definition le := bool_le. Definition lt := bool_lt. Theorem ordered : order A le. Proof. split. - unfold le ; intro x; case x; cbn in |- *; auto. - unfold le, transitive ; simple destruct x; simple destruct y; auto; simple destruct z; auto. - unfold le, antisymmetric; simple destruct x; simple destruct y; simpl in |- *; auto; contradiction. Qed.
imports: Relations List ZArith Arith