proposition: Lemma mult_ref0 : refines2 T1.T1mul T1mul.
proof: Proof. move => x y; move: x; induction y. - move => x; simpl h2g; rewrite T1mul_a0E; case x => //; by case. - case. + simpl h2g => // /=. + move => a n0 b. destruct (Epsilon0.T1.T1_eq_dec a Epsilon0.T1.zero). * subst; destruct (Epsilon0.T1.T1_eq_dec y1 Epsilon0.T1.zero). -- subst y1; simpl h2g; rewrite T1mul_cons_cons_E; congr cons; nia. -- repeat rewrite !h2g_cons !h2g_zero. rewrite T1mulE5. ++ rewrite multE5 => //. ** simpl h2g; simpl T1add; congr cons. destruct (Epsilon0.T1.T1_eq_dec y2 Epsilon0.T1.zero). { subst; by cbn. } { change (cons zero n0 (h2g b)) with (h2g (T1.cons Epsilon0.T1.zero n0 b)); now rewrite IHy2. } ++ destruct y1; [now destruct n1| now compute]. * destruct (Epsilon0.T1.T1_eq_dec y1 Epsilon0.T1.zero). -- subst; rewrite !h2g_cons !h2g_zero; rewrite T1mulE4. ++ by rewrite multE4. ++ by case :a n1 . -- rewrite !h2g_cons. ++ rewrite T1mulE5. ** rewrite multE5 => //. simpl h2g; rewrite plus_ref; congr cons. change (cons (h2g a) n0 (h2g b)) with (h2g (T1.cons a n0 b)); now rewrite IHy2. ** case: y1 n2 IHy1 => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)