proposition: Lemma remove_inv_prop : stable_expr remove_inv_func.
proof: Proof. intros [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; try apply refl_equal. destruct o ; try apply refl_equal. exact (Rmult_1_l _). Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library