proposition: Lemma hmult_dist : right_distributive T1mul T1add.
proof: Proof. move => a b c; move :(mul_distr (h2g a) (h2g b) (h2g c)) => H. rewrite -(g2h_h2gK a) -(g2h_h2gK b) -(g2h_h2gK c). by rewrite -!g2h_plusE -!g2h_multE H -g2h_plusE. Qed.
imports: mathcomp(all_ssreflect zify) gaia_hydras(T1Bridge ) hydras(T1) gaia(ssete9)