proposition: Lemma big_to_small : big_h -+-> small_h.
proof: Proof. unfold small_h; case_eq (m big_h); intros i j Hj; destruct i. - unfold big_h; right with (hyd1 (hyd1 head)). exists 0; right; left. left with (n:=0); split; left. destruct j. + now destruct m_big_h_not_null. + unfold iota;cbn;left. exists j;right; left; constructor 1; split; left. - unfold iota; cbn; destruct j. + left; unfold iota, big_h; cbn. exists i; right; left; left; split; left. + right with (iota (S (S i), 0)). unfold iota; simpl fst ; simpl snd; cbn; exists (S i); right. left; left; split; left. left; exists j; right; left; right. rewrite <- hcons_mult_comm; apply hcons_mult_S1. left; split; left. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)