Ord.base

Require Export mathcomp.ssreflect.ssreflect.
From mathcomp
  Require Export ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.

(*Require Import Coq.Program.Basics. (* flip *)*)
Require Export Coq.Setoids.Setoid. (* required for rewrite *)
Require Export Coq.Classes.Morphisms.
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Implicit Defensive.

Axiom functional_extensionality :
  forall (T : Type) (F : T -> Type) (f g : forall x, F x),
    (forall x, f x = g x) -> f = g.

Lemma fext {T} {F : T -> Type} (f g : forall x, F x) :
  (forall x, f x = g x) -> f = g.
Proof. apply: functional_extensionality. Qed.

Lemma all_xi {T} {F G : T -> Type} :
  (forall i, F i = G i) -> (forall i, F i) = (forall i, G i).
Proof.
  move=> h. apply fext in h. by rewrite h.
Qed.

Lemma all_xi_p {T} {F G : T -> Prop} :
  (forall i, F i = G i) -> (forall i, F i) = (forall i, G i).
Proof.
  move=> h. apply fext in h. by rewrite h.
Qed.

Axiom propositional_extensionality :
  forall (P Q : Prop), (P <-> Q) -> P = Q.

Lemma pext {P Q : Prop} :
  (P -> Q) -> (Q -> P) -> P = Q.
Proof.
  move=> pq qp. exact: propositional_extensionality.
Qed.

Lemma pi {P : Prop} (p q : P) : p = q.
Proof.
  have e: P = True by apply: pext. move: p q. by rewrite e => -[] [].
Qed.

Lemma sigma_eq (T : Type) (P : T -> Prop) (x y : { a : T | P a }) :
  (sval x = sval y) -> x = y.
Proof.
  move: x y => [a pa] [b pb] /= eqn. destruct eqn. f_equal. exact: pi.
Qed.

Definition Pred (T : Type) := T -> Prop.
Definition Rel (T : Type) := T -> Pred T.

Definition reflexive {T} (R : Rel T) := forall x, R x x.
Definition antisymmetric {T} (R : Rel T) := forall x y, R x y -> R y x -> x = y.
Definition transitive {T} (R : Rel T) := forall x y z, R x y -> R y z -> R x z.

Definition pairb {T} (x y : T) (b : bool) : T := if b then x else y.

Lemma pairb_fun {X Y} (f : X -> Y) x y :
  f \o pairb x y = pairb (f x) (f y).
Proof. by apply: fext => -[]. Qed.

Definition iprod {A} (B : A -> Type) := forall x, B x.

Definition is_prop (X : Type) := forall x y : X, x = y.

Ltac inv H := inversion H; clear H; subst.