Library gaia_hydras.GaiaToHydra

From mathcomp Require Import all_ssreflect zify.
From gaia_hydras Require Import T1Bridge .
From hydras Require Import T1.

From gaia Require Import ssete9.
Import Epsilon0.T1.

Locate T1.


Lemma hmultA : associative T1mul.

Example Ex1 (a: T1): T1omega × (a × T1omega) = T1omega × a × T1omega.

Lemma hmult_dist : right_distributive T1mul T1add.

Close Scope t1_scope.