proposition: Lemma oplusE (a b :T1) : a o+ b = match a, b with | zero, _ => b | _, zero => a | cons a1 n1 b1, cons a2 n2 b2 => match compare a1 a2 with | Gt => cons a1 n1 (b1 o+ b) | Eq => cons a1 (S (n1 + n2)) (b1 o+ b2) | Lt => cons a2 n2 (a o+ b2) end end.
proof: Proof. rewrite /oplus oplus_eqn; case: a. cbn ; by rewrite h2g_g2hK. case: b. move => ? ? ? ;by rewrite !h2g_g2hK. move => t n t0 t1 n0 t2; rewrite !g2h_cons compare_g2h. case (compare t1 t); by rewrite h2g_cons !h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg) gaia_hydras(T1Bridge)