proposition: Lemma mult_ref : refines2 T1.T1mul T1mul.
proof: Proof. Proof mult_ref0. Lemma g2h_multE (a b : T1) : g2h (a * b) = T1.T1mul (g2h a) (g2h b). Proof. apply symmetry, refines2_R, mult_ref. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)