proposition: Lemma R1_iff s s' : R1 (node s) (node s') <-> S0 s s'.
proof: Proof. split. - now inversion 1. - now constructor. Qed.
imports: Coq(Arith Lia List Relation_Operators Operators_Properties Peano_dec Wellfounded.Inverse_Image Wellfounded.Inclusion) hydras(More_Arith Epsilon0 Hessenberg Simple_LexProd MoreLibHyps)