Sum-product iso in Coq

prodsum.v

Section ProdSum.

Variables A B C : Prop.

Class Isomorphism A B :=
  MkIsomorphism {
    from: A -> B;
    to: B -> A;
    from_to b: from (to b) = b;
    to_from a: to (from a) = a
  }.

Definition fromPS : A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
by case=>a; case=>bc; [left|right].
Defined.

Definition toPS : (A /\ B) \/ (A /\ C) -> A /\ (B \/ C).
by case; case=>a bc; split=>//; [left|right].
Defined.

Theorem prodsum : Isomorphism (A /\ (B \/ C)) ((A /\ B) \/ (A /\ C)).
Proof.
have froto (sp : A /\ B \/ A /\ C): fromPS (toPS sp) = sp
  by move: sp; rewrite /fromPS /toPS; case; case.
have tofro (ps : A /\ (B \/ C)): toPS (fromPS ps) = ps
  by move: ps; rewrite /fromPS /toPS; case=>a; case.
apply: MkIsomorphism froto tofro.
Qed.

End ProdSum.