proposition: Remark Rem1 : {k:nat & {gamma: T1 | standard_path (S n) alpha k gamma /\ gamma t1< alpha}}.
proof: Proof. destruct (standard_path_to_zero n Halpha). - intro; subst; destruct (const_pathS_zero Hpa). - exists x, zero; split;auto. apply LT_trans with beta;auto. eapply const_pathS_LT; eauto. Defined.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)