proposition: Lemma demo_clears_all_and_clears_but : forall x y:nat, y < 2 -> x = x -> x >= 2 -> x < 3 -> True.
proof: Proof. Proof using. introv M1 M2 M3. dup 6. clears_all. auto. clears_but M3. auto. clears_but y. auto. clears_but x. auto. clears_but M2 M3. auto. clears_but x y. auto. Qed.
imports: Coq.Lists.List Coq.Logic.ProofIrrelevance Coq.Program.Equality Coq.Arith.Compare_dec Coq.micromega.Lia