proposition: Lemma minus_lt : forall a b, lt a b -> a - b = zero.
proof: Proof. induction a, b. 1-3: easy. - intro H. simpl. destruct a1, b1. + destruct (le_lt_dec n n0). 1: reflexivity. exfalso. apply lt_inv_coeff_dec in H as [Hlt | (Heq, Hlt)]; lia. + reflexivity. + apply lt_inv_strong in H as [Hlt | Heqa Hlt | Heqa Heqn Hlt]. * now apply compare_lt_iff in Hlt as ->. * apply compare_eq_iff in Heqa as ->. now apply Nat.compare_lt_iff in Hlt as ->. * apply compare_eq_iff in Heqa as ->. apply Nat.compare_eq_iff in Heqn as ->. now apply (IHa2 b2). + apply lt_inv_strong in H as [Hlt | Heqa Hlt | Heqa Heqn Hlt]. * now apply compare_lt_iff in Hlt as ->. * apply compare_eq_iff in Heqa as ->. now apply Nat.compare_lt_iff in Hlt as ->. * apply compare_eq_iff in Heqa as ->. apply Nat.compare_eq_iff in Heqn as ->. now apply (IHa2 b2). Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)