proposition: Lemma S0_remove_r : forall l , S0 (add_head_r l) l.
proof: Proof. induction l; simpl. - left. - now right. 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)